Commit 3bb673c8 authored by MARCHE Claude's avatar MARCHE Claude

updated roadmap

parent d5dd6cc2
......@@ -289,7 +289,7 @@ Scheduled for 31 october 2013
(i.e. si Coq a ete installé apres)
* Coq tactic (CLAUDE, GUILLAUME, JCF, ANDREI)
** bug Prod(_,_,_) -> traiter le cas
** DONE bug Prod(_,_,_) -> traiter le cas
* Smoke detector and absurd: on pourrait mettre un label particulier
sur le "false" genéré par absurd, pour indiquer que c'est
......@@ -315,9 +315,9 @@ Scheduled for 31 october 2013
* support for new provers
** Alt-Ergo 0.95.2 DONE
** CVC4 1.2 TODO: pb avec les booleens
** Coq 8.4pl2 TODO: probleme tactique Why3 ???
** Metitarski TODO: improve it (CLAUDE, GUILLAUME)
** others ?
** DONE Coq 8.4pl2: probleme tactique Why3
** DONE ? Metitarski: improve it (CLAUDE, GUILLAUME)
* DONE? simplification de (a && false) ne devrait pas etre false
......
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