diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 9 |
1 files changed, 7 insertions, 2 deletions
@@ -15,6 +15,8 @@ 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. + On by default and deprecated. Minor source of incompatibility + for code relying on the precise arguments of abstracted proofs. - 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 @@ -48,8 +50,11 @@ Hints Program -- The "Shrink Obligations" flag now applies to all obligations, not only those - solved by the automatic tactic. +- The "Shrink Obligations" flag now applies to all obligations, not only + those solved by the automatic tactic. +- "Shrink Obligations" is on by default and deprecated. Minor source of + incompatibility for code relying on the precise arguments of + obligations. Notations |