Commit e549f00f authored by MARCHE Claude's avatar MARCHE Claude

roadmap before release 0.71

parent 7838bc88
......@@ -91,6 +91,10 @@
*** add a tag to the git repository
*** The next commit : increment de why3 version
* YET TO DO
** fix bug with term shapes, not taking triggers into account
** remove prover coq-relize
* prover support
** DONE test/debug TPTP output, make Vampire work
......
......@@ -124,6 +124,7 @@ let rec t_shape ~(push:string->'a->'a) c m (acc:'a) t : 'a =
t_shape ~push c m (push tag_eps acc) f
| Tquant (q,b) ->
let vl,_,f1 = t_open_quant b in
(* TODO: take triggers into account !! *)
let m = vl_rename_alpha c m vl in
let hq = match q with Tforall -> tag_forall | Texists -> tag_exists in
push hq (t_shape ~push c m acc f1)
......
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