Commit 7226a369 authored by MARCHE Claude's avatar MARCHE Claude

updated roadmap

parent e8e631c9
......@@ -141,6 +141,31 @@ and no epsilon
==================== Roadmap for release 0.84 ========================
== TODOs ==
* verifier support des nouveaux prouveurs: Coq8.4pl4, Isabelle-2014,
CVC4 1.4, yices2 (quantifiers ?) beagle ? driver TPTP TFA ? autres ?
* completer le fichier CHANGES
** nouvelle facon d'appeler les outils "why3 xxx ..."
** strategies de preuve
** transformation "compute_in_goal"
** support de nouveaux prouveurs
** nouvelle structure des fichiers de session et de shape (compatibilité)
** new examples ?
* ajouter dans les instructions de release ci-dessous la procedure de
fabrication du paquet opam
* documentation des nouvelles features higher-order
* eliminate_match:
** faire un cas particulier pour "bool", le match pouvant se traduire
vers ite qui est supporté par pas mal de prouveurs
** introduire des symboles _match non polymorphes differents pour
chaque instance necessaires. plutot qu'un seul symbole _match
polymorphe.
== New Features to announce ==
See CHANGES
......@@ -224,16 +249,6 @@ See CHANGES
* The next commit : add +git to the version in file Version
== TODOs ==
* documentation des nouvelles features higher-order
* eliminate_match:
** faire un cas particulier pour "bool", le match pouvant se traduire
vers ite qui est supporté par pas mal de prouveurs
** introduire des symboles _match non polymorphes differents pour
chaque instance necessaires. plutot qu'un seul symbole _match
polymorphe.
==================== Roadmap for release 0.83 ========================
......
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