diff options
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 98 |
1 files changed, 51 insertions, 47 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index b5d94d58..b44f344d 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -1,58 +1,62 @@ -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 +Tactics -- Inductive types in Type are now polymorphic over their parameters in - Type. This may 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 - hypotheses that are later refered to in the proof script. +- 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. + +- The default relation chosen by setoid_replace may differ. The + workaround is to enforce the choice of the setoid relation with the + "using relation ..." option. + +- The ordering of subgoals generated by setoid_rewrite and + setoid_replace tactics has been changed. Some reordering in the + proof script may be necessary. You may also use the 'by ...' option + of setoid_replace and setoid_rewrite. + +- The definition of Setoid_Theory has changed. When using the + constructors of the structure, you need to unfold the definitions + Reflexive, Symmetric, and Transitive. + +- The names of bound variables of theorems generated by Add Morphism + differs, which may cause some problems with scripts that do not name + variable when perform introductions. Changing intros to the + appropriate intro x x0 ... xn should fix the problem. + +- Tactic firstorder "with" and "using" options have their meaning + swapped for consistency with auto/eauto. The solution is to swap + the use of these options in call to firstorder. + +- Introduction patterns are more strict. In "intros [ ... | ... | ... ] H", + the names in the brackets are synchronized so that H denotes the same + hypothesis in every subgoal. + +- Some bug fixes may lead to incompatibilities (see CHANGES for a detailed + account). -Tactics +Language -- 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. +- 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. Libraries -- A few 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. +- Some changes in the library (as mentioned in the CHANGES file) may + imply the need for local adaptations. This may particularly be the + case with the move from Set to Type in libraries FSets, SetoidList, + ListSet, Sorting and Zmisc. In case of trouble it may help to simply + declare Set as an alias for Type (see file SetIsType). -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. |