diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | COMPATIBILITY | 21 |
2 files changed, 24 insertions, 0 deletions
@@ -90,6 +90,9 @@ Tactics - "change ... in ..." and "simpl ... in ..." now consider nested occurrences (possible source of incompatibilities since this alters the numbering of occurrences). +- The "change p with c" tactic semantics changed, now typechecking + "c" at each matching occurrence "t" of the pattern "p", and + converting "t" with "c". - Now "appcontext" and "context" behave the same. The old buggy behaviour of "context" can be retrieved at parse time by setting the "Tactic Compat Context" flag. (possible source of incompatibilities). diff --git a/COMPATIBILITY b/COMPATIBILITY index 3c9a94fae2..33bb1d30ee 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -1,3 +1,24 @@ +Potential sources of incompatibilities between Coq V8.4 and V8.5 +---------------------------------------------------------------- + +Universe Polymorphism. + +- Refinement, unification and tactics are now aware of universes, + resulting in more localized errors. Universe inconsistencies + should no more get raised at Qed time but during the proof. + Unification *always* produces well-typed substitutions, hence + some rare cases of unifications that succeeded while producing + ill-typed terms before will now fail. + +- The [change p with c] tactic semantics changed, now typechecking + [c] at each matching occurrence [t] of the pattern [p], and + converting [t] with [c]. + +- Template polymorphic inductive types: the partial application + of a template polymorphic type (e.g. list) is not polymorphic. + An explicit parameter application (e.g [fun A => list A]) or + [apply (list _)] will result in a polymorphic instance. + Potential sources of incompatibilities between Coq V8.3 and V8.4 ---------------------------------------------------------------- |