Improving compatibility between 8.2 and 8.3

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12904 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 35 insertions, 56 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index b44f344d4..9f11d986e 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -1,62 +1,41 @@
-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)
 
+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]
+
 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 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).
-
-Language
-
-- 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]