diff options
| author | Guillaume Melquiond | 2015-12-16 18:30:32 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-12-16 18:30:32 +0100 |
| commit | b8d1e84e9326df34383e5e5c8c5842cb7013b935 (patch) | |
| tree | d3783da15f09d47b1002b2ed31385f897e8bd4bf /CHANGES | |
| parent | 53ab313dcf7ae524a9a8312658c1e9869a4039f7 (diff) | |
Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 14 |
1 files changed, 9 insertions, 5 deletions
@@ -1,11 +1,12 @@ Changes from V8.5beta3 ====================== -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 @@ -21,6 +22,9 @@ Tactics 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 =================================== |