Commit c3fd2d7b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove support for Coq 8.3.

parent 9eff56b9
......@@ -462,11 +462,6 @@ else
COQVERSION=`$COQC -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
case $COQVERSION in
8.3*)
enable_coq_support=yes
coq_compat_version=".8.3"
AC_MSG_RESULT($COQVERSION)
;;
8.4*|trunk)
enable_coq_support=yes
coq_compat_version=".8.4"
......@@ -474,8 +469,8 @@ else
;;
*)
enable_coq_support=no
AC_MSG_WARN(You need Coq 8.3 or later; Coq discarded)
reason_coq_support=" (version is $COQVERSION but need version 8.3 or higher)"
AC_MSG_WARN(You need Coq 8.4 or later; Coq discarded)
reason_coq_support=" (version is $COQVERSION but need version 8.4 or higher)"
;;
esac
fi
......
......@@ -5,7 +5,7 @@
\subsubsection{Installation}
You need Coq version 8.3 or greater. If this is the case, \why's
You need Coq version 8.4 or greater. If this is the case, \why's
configuration detects it, then compiles and installs the Coq tactic.
The Coq tactic is installed in
\begin{center}
......
......@@ -267,6 +267,33 @@ theory real.PowerInt
end
theory real.Trigonometry
prelude "Require Reals.Rtrigo_def."
prelude "Require Reals.Rtrigo1."
prelude "Require Reals.Ratan."
syntax function cos "(Reals.Rtrigo_def.cos %1)"
syntax function sin "(Reals.Rtrigo_def.sin %1)"
syntax function pi "Reals.Rtrigo1.PI"
syntax function tan "(Reals.Rtrigo1.tan %1)"
syntax function atan "(Reals.Ratan.atan %1)"
remove prop Pythagorean_identity
remove prop Cos_le_one
remove prop Sin_le_one
remove prop Cos_0
remove prop Sin_0
remove prop Cos_pi
remove prop Sin_pi
remove prop Cos_pi2
remove prop Sin_pi2
end
theory list.List
syntax type list "(list %1)"
......
......@@ -9,29 +9,3 @@ transformation "inline_trivial"
transformation "eliminate_builtin"
import "coq-common.gen"
theory real.Trigonometry
prelude "Require Import Rtrigo."
prelude "Require Import AltSeries. (* for def of pi *)"
syntax function cos "(Rtrigo_def.cos %1)"
syntax function sin "(Rtrigo_def.sin %1)"
syntax function pi "PI"
syntax function tan "(Rtrigo.tan %1)"
(* syntax function atan "atan not defined in Coq ?" *)
remove prop Pythagorean_identity
remove prop Cos_le_one
remove prop Sin_le_one
remove prop Cos_0
remove prop Sin_0
remove prop Cos_pi
remove prop Sin_pi
remove prop Cos_pi2
remove prop Sin_pi2
end
prelude "(* This file is generated by Why3's Coq 8.4 driver *)"
prelude "(* Beware! Only edit allowed sections below *)"
printer "coq"
filename "%f_%t_%g.v"
transformation "inline_trivial"
transformation "eliminate_builtin"
import "coq-common.gen"
theory real.Trigonometry
prelude "Require Import Rtrigo."
prelude "Require Import AltSeries. (* for def of pi *)"
syntax function cos "(Rtrigo_def.cos %1)"
syntax function sin "(Rtrigo_def.sin %1)"
syntax function pi "PI"
syntax function tan "(Rtrigo1.tan %1)"
syntax function atan "(Ratan.atan %1)"
remove prop Pythagorean_identity
remove prop Cos_le_one
remove prop Sin_le_one
remove prop Cos_0
remove prop Sin_0
remove prop Cos_pi
remove prop Sin_pi
remove prop Cos_pi2
remove prop Sin_pi2
end
......@@ -418,21 +418,6 @@ version_ok = "8.4pl2"
version_ok = "8.4pl1"
version_ok = "8.4"
command = "%l/why3-cpulimit 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
driver = "drivers/coq_8_4.drv"
editor = "coqide"
[ITP coq]
name = "Coq"
compile_time_support = true
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.3pl4"
version_ok = "8.3pl3"
version_ok = "8.3pl2"
version_ok = "8.3pl1"
version_ok = "8.3"
command = "%l/why3-cpulimit 0 %m -s %e -I %l/coq-tactic -R %l/coq Why3 -l %f"
driver = "drivers/coq.drv"
editor = "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