diff options
| -rw-r--r-- | CHANGES | 49 |
1 files changed, 23 insertions, 26 deletions
@@ -1,24 +1,9 @@ Changes from V8.4 ================= -Vernacular commands - -- Undo and UndoTo are now handling the proof states. They may - perform some extra steps of backtrack to avoid states where - the proof state is unavailable (typically a closed proof). -- The commands Suspend and Resume have been removed. -- A basic Show Script has been reintroduced (no indentation). - Tactics - Tactics btauto, a reflexive boolean tautology solver. -- Still no general "info" tactical, but new specific tactics - info_auto, info_eauto, info_trivial which provides information - on the proofs found by auto/eauto/trivial. Display of these - details could also be activated by Set Info Auto/Eauto/Trivial. -- Details on everything tried by auto/eauto/trivial during - a proof search could be obtained by "debug auto", "debug eauto", - "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial". Program @@ -26,17 +11,6 @@ Program consistent with "Proof with". - Program Lemma, Definition now respect automatic introduction. -Module System - -- The names of modules (and module types) are now in a fully separated - namespace from ordinary definitions : "Definition E:=0. Module E. End E." - is now accepted. - -CoqIDE - -- Coqide now supports the Restart command, and Undo (with a warning). - Better support for Abort. - Notations - "Bind Scope" can no longer bind "Funclass" and "Sortclass". @@ -46,6 +20,11 @@ Changes from V8.4beta to V8.4 Vernacular commands +- Undo and UndoTo are now handling the proof states. They may + perform some extra steps of backtrack to avoid states where + the proof state is unavailable (typically a closed proof). +- The commands Suspend and Resume have been removed. +- A basic Show Script has been reintroduced (no indentation). - New command "Set Parsing Explicit" for deactivating parsing (and printing) of implicit arguments (useful for teaching). - New command "Grab Existential Variables" to transform the unresolved evars at @@ -53,9 +32,27 @@ Vernacular commands Tactics +- Still no general "info" tactical, but new specific tactics + info_auto, info_eauto, info_trivial which provides information + on the proofs found by auto/eauto/trivial. Display of these + details could also be activated by Set Info Auto/Eauto/Trivial. +- Details on everything tried by auto/eauto/trivial during + a proof search could be obtained by "debug auto", "debug eauto", + "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial". - New command "r string" that interprets "idtac string" as a breakpoint and jumps to its next use in Ltac debugger. +Module System + +- The names of modules (and module types) are now in a fully separated + namespace from ordinary definitions : "Definition E:=0. Module E. End E." + is now accepted. + +CoqIDE + +- Coqide now supports the Restart command, and Undo (with a warning). + Better support for Abort. + Changes from V8.3 to V8.4beta ============================= |