Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

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.