MAJ

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

1 files changed, 28 insertions, 2 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index bb293baa9..b5d94d584 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -3,6 +3,8 @@ Potential sources of incompatibilities between Coq V8.0 and V8.1
 
 (see also file CHANGES)
 
+Language
+
 - 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
@@ -10,6 +12,8 @@ Potential sources of incompatibilities between Coq V8.0 and V8.1
   a matter of fact, it is recommended to systematically name the
   hypotheses that are later refered to in the proof script.
 
+Tactics
+
 - 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.
@@ -21,6 +25,28 @@ Potential sources of incompatibilities between Coq V8.0 and V8.1
   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.
+
+Libraries
+
 - A few changes in the library (as mentioned in the CHANGES file) may
   imply the need for local adaptations.
 
@@ -28,5 +54,5 @@ Potential sources of incompatibilities between Coq V8.0 and V8.1
   match construction: occurrences in the return clause now come after
   the occurrences in the term matched; this was the opposite before.
 
-- For changes in the ML interfaces, see file dev/doc/changes.txt in
-  the main archive.
+For changes in the ML interfaces, see file dev/doc/changes.txt in the
+main archive.