diff options
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 114 |
1 files changed, 48 insertions, 66 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index 30f5daf8..09b72e92 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -1,72 +1,54 @@ -Potential sources of incompatibilities between Coq V8.1 and V8.2 +Potential sources of incompatibilities between Coq V8.2 and V8.3 ---------------------------------------------------------------- (see also file CHANGES) +The main incompatibilities between 8.2 and 8.3 are the following + +- When defining objects using tactics as in "Definition f binders : + type.", the binders are automatically introduced in the context. The + former behavior can be restored by using "Unset Automatic + Introduction" (for local modification) or "Global Unset Automatic + Introduction" (for inheritance through Require). + +- For setoid rewriting, Morphism has been renamed into Proper. + +In general, most sources of incompatibilities can be avoided by +calling coqtop or coqc with option "-compat 8.2". The sources of +incompatibilities listed below must however be treated manually. + +Syntax + +- The word "by" is now a keyword and can no longer be used as an identifier. + [Semantics, IEEE754] + +Type inference + +- Many changes in using classes. [ATBR] + +Library + +- New identifiers of the library can hide identifiers. This can be + solved by changing the order of Require or by qualifying the + identifier with the name of its module. [Stalmarck] + +- Reorganisation of library (esp. FSets, Sorting, Numbers) may have + moved or removed names around. [FundamentalArithmetics, CoLoR, + Icharate, AMM11262, FSets, FingerTree] + +- Infix notation "++" has now to be set at level 60. [LinAlg] + +- When using Program (refl_equal and Vnil have maximal implicit + arguments, lemmas about measure have a different form, ...). + Tactics -- 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 constant [flip] is automatically unfolded in the goals generated by - Add Morphism (incompatibility with 8.2 beta versions). - -- 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. - -- Application patterns with a meta variable in function position (?X ?Y) now - match arbitrary applications as expected. Use a nested - [match X with (_ _) => fail 1 | _ => ..] to recover the old semantics. - -- Some bug fixes may lead to incompatibilities (see CHANGES for a detailed - account). - -Language - -- Type Class syntax has completely since the 8.2beta versions. See the - documentation for the updated syntax. - -- 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 - -- 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 the main changes in the ML interfaces, see file -dev/doc/changes.txt in the main archive. +- The synchronization of introduction names and quantified hypotheses + names may exceptionally lead to different names in "induction" + (usually a name with lower index is required). [Automata] + +- More checks in some commands (e.g. in Hint) may lead to forbid some + meaningless part of them. [CoLoR] + +- When rewriting using setoid equality, the default equality found + might be different. [CoRN] |