Commit d666f4f2 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

restored PVS support after release

parent bfeed852
...@@ -625,15 +625,15 @@ if test "$enable_coq_support" = "yes" ; then ...@@ -625,15 +625,15 @@ if test "$enable_coq_support" = "yes" ; then
echo " FP arithmetic : $enable_coq_fp_libs $reason_coq_fp_libs" echo " FP arithmetic : $enable_coq_fp_libs $reason_coq_fp_libs"
fi fi
fi fi
dnl echo "PVS support : $enable_pvs_support $reason_pvs_support" echo "PVS support : $enable_pvs_support $reason_pvs_support"
dnl if test "$enable_pvs_support" = "yes" ; then if test "$enable_pvs_support" = "yes" ; then
dnl echo " Version : $PVSVERSION" echo " Version : $PVSVERSION"
dnl echo " Lib : $PVSLIB" echo " Lib : $PVSLIB"
dnl echo " Realization support : $enable_pvs_libs $reason_pvs_libs" echo " Realization support : $enable_pvs_libs $reason_pvs_libs"
dnl if test "$enable_pvs_libs" = "yes" ; then if test "$enable_pvs_libs" = "yes" ; then
dnl echo " FP arithmetic : $enable_pvs_fp_libs $reason_pvs_fp_libs" echo " FP arithmetic : $enable_pvs_fp_libs $reason_pvs_fp_libs"
dnl fi fi
dnl fi fi
echo "hypothesis selection : $enable_hypothesis_selection" echo "hypothesis selection : $enable_hypothesis_selection"
echo "debugging symbols : $enable_debug" echo "debugging symbols : $enable_debug"
echo "profiling : $enable_profiling" echo "profiling : $enable_profiling"
......
...@@ -88,7 +88,7 @@ much about comments. For instance, \why can easily be confused by ...@@ -88,7 +88,7 @@ much about comments. For instance, \why can easily be confused by
some terminating directive like \verb+Qed+ that would be present in a some terminating directive like \verb+Qed+ that would be present in a
comment. comment.
% \input{./pvs.tex} \input{./pvs.tex}
\section{Shipping libraries of realizations} \section{Shipping libraries of realizations}
......
...@@ -346,19 +346,19 @@ command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 ...@@ -346,19 +346,19 @@ command = "'@LOCALBIN@why3-cpulimit' 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3
driver = "drivers/coq.drv" driver = "drivers/coq.drv"
editor = "coqide" editor = "coqide"
# [ITP pvs] [ITP pvs]
# name = "PVS" name = "PVS"
# exec = "pvs" exec = "pvs"
# version_switch = "-version" version_switch = "-version"
# version_regexp = "PVS Version \\([^ \n]+\\)" version_regexp = "PVS Version \\([^ \n]+\\)"
# version_ok = "5.0" version_ok = "5.0"
# command = "'@LOCALBIN@why3-cpulimit' 0 %m -s @LOCALBIN@why3-check-pvs %l %f" command = "'@LOCALBIN@why3-cpulimit' 0 %m -s @LOCALBIN@why3-check-pvs %l %f"
# driver = "drivers/pvs.drv" driver = "drivers/pvs.drv"
# editor = "pvs" editor = "pvs"
# [editor pvs] [editor pvs]
# name = "PVS" name = "PVS"
# command = "@LOCALBIN@why3-call-pvs %l %f" command = "@LOCALBIN@why3-call-pvs %l %f"
[editor coqide] [editor coqide]
name = "CoqIDE" name = "CoqIDE"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment