- Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"

  n'étaient pas gérés, merci à Julien). 
- Correction pb blocage CoqIDE quand le browser n'est pas déja lancé
  (utilisation pour cela de Sys.command au lieu de Unix.open_process_full).
- MAJ CHANGES et COMPATIBILITY.


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

1 files changed, 15 insertions, 40 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index b5d94d584..7ddc33d47 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -1,12 +1,12 @@
-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
 
-- Inductive types in Type are now polymorphic over their parameters in
-  Type. This may affect the naming of introduction hypotheses if such
+- 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.  As
   a matter of fact, it is recommended to systematically name the
@@ -14,45 +14,20 @@ Language
 
 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.
-
-- 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.
+- 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.
+
+- Some bug fixes may lead to incompatibilities.
 
 Libraries
 
-- A few changes in the library (as mentioned in the CHANGES file) may
+- Some 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.
-
-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.