Commit 98a436ee authored by MARCHE Claude's avatar MARCHE Claude

updated roadmap after Why3 GT

parent d07a1f53
......@@ -161,7 +161,12 @@ Release Notes (details in file CHANGES):
* fix bug 18953 : (<>) not allowed as prefix form
* finalize detect_polymorphism. Allow polymorphic tuples (supported by SMT ?)
solution possible: symbol builtin t_neq, inlining systematique au typage
(ou laisser inline_trivial le faire)
* DONE finalize detect_polymorphism. Allow polymorphic tuples (supported by SMT ?)
C'est finalisé. Mais les tuples restent polymorphes.
* integrate server feature done by Johannes
......@@ -180,6 +185,8 @@ Release Notes (details in file CHANGES):
alt-ergo -replay <file>.agr
-> on pourrait le faire en considerant altgr-ergo comme un prouveur interactif
* make the strategy feature public and documented. Possibly generate
default strategies dynamically at the time of why3 config --detect,
using the provers detected : for that, we can annotated the provers in
......
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