Commit 54f72bbf authored by MARCHE Claude's avatar MARCHE Claude

changes

parent 8e45430a
......@@ -3,11 +3,12 @@ version 0.64, Feb 16, 2011
==========================
o algebraic types: must be well-founded, non-positive constructors
are forbidden, recursive functions and predicates must
are forbidden, recursive functions and predicates must
structurally terminate
o syntax: /\ renamed into && and \/ into ||
o accept lowercase names for axioms, lemmas, goals
o labels in terms and formulas are not printed anymore
o accept lowercase names for axioms, lemmas, goals, and cases in
inductive predicates
o labels in terms and formulas are not printed by default.
o transformation split-goal does not split under disjunction anymore
o fixed --enable-local
o why.conf is no more looked for in the current directory; use -C or
......@@ -19,9 +20,9 @@ version 0.64, Feb 16, 2011
--autodetect-plugins renamed to --detect-plugins
new option --detect to perform both detections
o why3config: --conf_file is replaced by -C and --config
o TPTP: encoding by explicit polymorphism is not anymore the
o TPTP: encoding by explicit polymorphism is not anymore the
default encoding for TPTP provers. It is now forbidden to use this
encoding in presence of finite types.
encoding in presence of finite types.
o IDE: source file names are stored in database with paths relative
to the database, so that databases are now easier to move from a
machine to another (e.g when they are stored in source control
......
......@@ -17,6 +17,7 @@ will get a error message because of missing loadpath to modules
** in IDE: replay all obsolete but previously successful proofs
** in whybench
** add replay of existing proofs in "make bench" to detect regression
** add automatic recompilation, install and bench every night on moloch
* IDE: implement "inline" (use transformation inline_goal)
** partially done
......
......@@ -527,8 +527,10 @@ open Theory
let print_tdecl ~old info fmt d = match d.td_node with
| Decl d -> print_decl ~old info fmt d
| Use t ->
| Use _t -> ()
(*
fprintf fmt "Require Import %s.@\n@\n" (id_unique iprinter t.th_name)
*)
| Meta _ -> assert false (* TODO ? *)
| Clone _ -> assert false (* TODO *)
......
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