diff options
| -rw-r--r-- | CHANGES | 9 | ||||
| -rw-r--r-- | COMPATIBILITY | 14 |
2 files changed, 21 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 diff --git a/COMPATIBILITY b/COMPATIBILITY index 883b8576d..892eaa599 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -1,3 +1,17 @@ +Potential sources of incompatibilities between Coq V8.5 and V8.6 +---------------------------------------------------------------- + +Symptom: An obligation generated by Program or an abstracted subproof +has different arguments. +Cause: Set Shrink Abstract and Set Shrink Obligations are on by default +and the subproof does not use the argument. +Remedy: +- Adapt the script. +- Write an explicit lemma to prove the obligation/subproof and use it + instead (compatible with 8.4). +- Unset the option for the program/proof the obligation/subproof originates + from. + Potential sources of incompatibilities between Coq V8.4 and V8.5 ---------------------------------------------------------------- |