diff options
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 55 |
1 files changed, 15 insertions, 40 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index b5d94d584b..7ddc33d47f 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -1,12 +1,12 @@ -Potential sources of incompatibilities between Coq V8.0 and V8.1 +Potential sources of incompatibilities between Coq V8.1 and V8.2 ---------------------------------------------------------------- (see also file CHANGES) Language -- Inductive types in Type are now polymorphic over their parameters in - Type. This may affect the naming of introduction hypotheses if such +- Constants hidding polymorphic inductive types are now polymorphic themselves. + This may exceptionally affect the naming of introduction hypotheses if such an inductive type in Type is used on small types such as Prop or Set: the hypothesis names suffix will default to H instead of X. As a matter of fact, it is recommended to systematically name the @@ -14,45 +14,20 @@ Language Tactics -- Some bug fixes may lead to incompatibilities. This is e.g. the case - of inversion on Type which failed to rewrite some hypotheses as it - did on Prop/Set. - -- Add Morphism for the Prop/iff setoid now requires a proof of - biimplication instead of a proof of implication. - -- The order of arguments in compatibility morphisms changed: the - premises and the parameters are now interleaved while the whole - bunch of parameters used to come first. - -- The previous implementation of the ring and field tactics are - maintained but their name changed : require modules "LegacyRing" or - "LegacyField" and globally replace calls to "ring" and "field" by - calls to "legacy ring" and "legacy field". - -- Users ready to benefit of the power of the new implemetations have - to know that - - - most of the time, ring solves goals similarly and often faster; - - if not, it may be because the old ring did some automatic unfold; - they now have to be done separately (by hand or using ltac); - - most of the time, field solvesp goals similarly but much faster but - there are usually less side conditions to prove; - - to simplify expressions, use now ring_simplify and field_simplify; - - simplifications are most of the time different: the new results are - more natural but they may require some adaptation of proof scripts; - - the Ring library no longer imports the Bool library (you may have - to explicitly request a "Require Import Bool"); - - to declare new rings and fields, see the documentation. +- The apply tactic now unfolds the constants if needed to succeed. As + a consequence, use of "try apply" or "repeat apply" or "apply" in + other Ltac potentially backtracking code may behave differently. Use + "simple apply" instead. + +- Add Relation and Add Morphism on polymorphic relations should now be + declared with Add Parametric Relation and Add Parametric Morphism. + +- Some bug fixes may lead to incompatibilities. Libraries -- A few changes in the library (as mentioned in the CHANGES file) may +- Some changes in the library (as mentioned in the CHANGES file) may imply the need for local adaptations. -- Occurrence numbering order for unfold, pattern, etc changed for the - match construction: occurrences in the return clause now come after - the occurrences in the term matched; this was the opposite before. - -For changes in the ML interfaces, see file dev/doc/changes.txt in the -main archive. +For the main changes in the ML interfaces, see file +dev/doc/changes.txt in the main archive. |