Commit 5974d37e authored by MARCHE Claude's avatar MARCHE Claude

fixed last bugs before release

parent 70f13db7
......@@ -89,11 +89,11 @@
** The last commit:
*** increment the magic number in config
*** add a tag to the git repository
*** The next commit : increment de why3 version
*** The next commit : increment why3 version
* YET TO DO
** fix bug with term shapes, not taking triggers into account
** remove prover coq-relize
* misc
** DONE fix bug with term shapes, not taking triggers into account
** DONE remove prover coq-realize
* prover support
** DONE test/debug TPTP output, make Vampire work
......
......@@ -10,10 +10,6 @@
id="coq"
name="Coq"
version="8.2pl1"/>
<prover
id="coq-realize"
name="Coq Realize"
version="8.2pl1"/>
<prover
id="cvc3"
name="CVC3"
......
......@@ -169,23 +169,6 @@ version_old = "1.3"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt %f"
driver = "drivers/z3_smtv1.drv"
[ITP coq-realize]
name = "Coq Realize"
exec = "coqc"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.3pl2"
version_ok = "8.3pl1"
version_ok = "8.3"
version_ok = "8.2pl2"
version_ok = "8.2pl1"
version_ok = "8.2"
version_old = "8.1"
version_old = "8.0"
command = "@LOCALBIN@why3-cpulimit 0 %m -s %e %f"
driver = "drivers/coq-realize.drv"
editor = "coqide"
[ITP coq]
name = "Coq"
exec = "coqc"
......
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