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

3 files changed, 40 insertions, 58 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index b44f344d43..9f11d986e5 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]
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index eb1d1985ff..dac435e7fd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -413,7 +413,8 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
 
 let find_appl_head_data = function
   | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
-  | RApp (_,RRef (_,ref),l) as x when l <> [] ->
+  | RApp (_,RRef (_,ref),l) as x
+      when l <> [] & Flags.version_strictly_greater Flags.V8_2 ->
       let n = List.length l in
       x,list_skipn_at_least n (implicits_of_global ref),
       list_skipn_at_least n (find_arguments_scope ref),[]
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 307aa7797d..8a4fb392ea 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -182,7 +182,9 @@ let find_elim hdcncl lft2rgt dep cls args gl =
   let inccl = (cls = None) in
   if (hdcncl = constr_of_reference (Coqlib.glob_eq) ||
       hdcncl = constr_of_reference (Coqlib.glob_jmeq) &&
-      pf_conv_x gl (List.nth args 0) (List.nth args 2)) && not dep then
+      pf_conv_x gl (List.nth args 0) (List.nth args 2)) && not dep
+    || Flags.version_less_or_equal Flags.V8_2
+  then
     (* use eq_rect, eq_rect_r, JMeq_rect, etc for compatibility *)
     let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
     let hdcncls = string_of_inductive hdcncl ^ suffix in