Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 2 insertions, 48 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 4cc8b589..0849b64f 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -1,52 +1,6 @@
-Potential sources of incompatibilities between Coq V8.2 and V8.3
+Potential sources of incompatibilities between Coq V8.3 and V8.4
 ----------------------------------------------------------------
 
 (see also file CHANGES)
 
-The main incompatibilities between 8.2 and 8.3 are the following
-
-- When defining objects using tactics as in "Definition f binders :
-  type.", the binders are automatically introduced in the context. The
-  former behavior can be restored by using "Unset Automatic
-  Introduction" (for local modification) or "Global Unset Automatic
-  Introduction" (for inheritance through Require).
-
-- For setoid rewriting, Morphism has been renamed into Proper.
-
-In general, 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.
-
-Type inference
-
-- Many changes in using classes.
-
-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.
-
-- Reorganisation of library (esp. FSets, Sorting, Numbers) may have
-  changed or removed names around.
-
-- Infix notation "++" has now to be set at level 60. [LinAlg]
-
-- When using the Programs library or any feature that uses it,
-  (lemmas about measure have a different form, ...).
-
-Tactics
-
-- 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).
-
-- More checks in some commands (e.g. in Hint) may lead to forbid some
-  meaningless part of them.
-
-- When rewriting using setoid equality, the default equality found
-  might be different.
+TO BE DONE