Quelques infos pour la portabilité 8.1 --> 8.2

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

1 files changed, 18 insertions, 0 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 159544529..1ed4b25d0 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -22,6 +22,24 @@ Tactics
 - 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.
+
 - Some bug fixes may lead to incompatibilities (see CHANGES for a detailed
   account).