diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 19 |
1 files changed, 12 insertions, 7 deletions
@@ -12,14 +12,15 @@ Program - The "Shrink Obligations" flag now applies to all obligations, not only those solved by the automatic tactic. -Changes from V8.5beta3 -====================== +Changes from V8.5beta3 to V8.5 +============================== -Vernacular commands -- Flag -compat 8.4 now loads Coq.Compat.Coq84. The standard way of putting Coq - in v8.4 compatibility mode is to pass the command line flag "-compat 8.4". It - can be followed by "-require Coq.Compat.AdmitAxiom" if 8.4 behavior of admit is - needed, in which case it uses an axiom. +Tools + +- Flag "-compat 8.4" now loads Coq.Compat.Coq84. The standard way of + putting Coq in v8.4 compatibility mode is to pass the command line flag + "-compat 8.4". It can be followed by "-require Coq.Compat.AdmitAxiom" + if the 8.4 behavior of admit is needed, in which case it uses an axiom. Specification language @@ -34,6 +35,10 @@ Tactics - Syntax "p/c" for on-the-fly application of a lemma c before introducing along pattern p changed to p%c1..%cn. The feature and syntax are in experimental stage. +- "Proof using" does not clear unused section variables. +- "refine" has been changed back to the 8.4 behavior of shelving subgoals + that occur in other subgoals. The "refine" tactic of 8.5beta2 has been + renamed "simple refine"; it does not shelve any subgoal. Changes from V8.5beta2 to V8.5beta3 =================================== |