diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 28 |
1 files changed, 28 insertions, 0 deletions
@@ -1,3 +1,24 @@ +Changes beyond V8.5 +=================== + +Tactics + +- Flag "Bracketing Last Introduction Pattern" is now on by default. +- New flag "Shrink Abstract" that minimalizes proofs generated by the abstract + tactical w.r.t. variables appearing in the body of the proof. +- Serious bugs are fixed in tactic "double induction" (source of + incompatibilities as soon as the inductive types have dependencies in + the type of their constructors; "double induction" remains however + deprecated). +- In introduction patterns of the form (pat1,...,patn), n should match + the exact number of hypotheses introduced (except for local definitions + for which pattern can be omitted, as in regular pattern-matching). + +Program + +- The "Shrink Obligations" flag now applies to all obligations, not only those + solved by the automatic tactic. + Changes from V8.5beta3 to V8.5 ============================== @@ -63,6 +84,13 @@ Tactics "intros" automatically complete the introduction of its subcomponents, as the the disjunctive-conjunctive introduction patterns in non-terminal position already do. +- New flag "Shrink Abstract" that minimalizes proofs generated by the abstract + tactical w.r.t. variables appearing in the body of the proof. + +Program + +- The "Shrink Obligations" flag now applies to all obligations, not only those +solved by the automatic tactic. - Importing Program no longer overrides the "exists" tactic (potential source of incompatibilities). - Hints costs are now correctly taken into account (potential source of |