Commit 025a3918 authored by Allan Blanchard's avatar Allan Blanchard

[wp] Fixes Coq compilation constraints

parent 3c57dedd
......@@ -132,6 +132,6 @@ depopts: [
messages: [
"The Frama-C/Wp now uses Why-3 for all provers (Cf. deprecated -wp-prover native:alt-ergo)"
{alt-ergo:installed}
"The Frama-C/Wp native support for Coq is now deprecated (use TIP or Why-3 instead)."
"The Frama-C/Wp native support for Coq is deprecated and only activated with Coq.8.12.x (use TIP or Why-3 instead)."
{coq:installed}
]
......@@ -85,16 +85,14 @@ if test "$ENABLE_WP" != "no"; then
if test "$COQC" = "yes" ; then
COQVERSION=`coqc -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
case $COQVERSION in
8.7*|8.8*|8.9*|8.10*|8.11.*|8.12.*|trunk)
8.12.*|trunk)
AC_MSG_RESULT(coqc version $COQVERSION found)
;;
*)
AC_MSG_RESULT(unsupported coqc version $COQVERSION)
AC_MSG_RESULT(unsupported coqc version $COQVERSION for - deprecated - native backend)
COQC="no"
;;
esac
else
AC_MSG_NOTICE(rerun configure to make wp using coq 8.7.2 or higher)
fi
else
COQC="no"
......
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