Imported Upstream version 8.3upstream/8.3

1 files changed, 8 insertions, 10 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 09b72e92..4cc8b589 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -20,35 +20,33 @@ 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.
-  [Semantics, IEEE754]
 
 Type inference
 
-- Many changes in using classes. [ATBR]
+- 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.  [Stalmarck]
+  identifier with the name of its module.
 
 - Reorganisation of library (esp. FSets, Sorting, Numbers) may have
-  moved or removed names around. [FundamentalArithmetics, CoLoR,
-  Icharate, AMM11262, FSets, FingerTree]
+  changed or removed names around.
 
 - Infix notation "++" has now to be set at level 60. [LinAlg]
 
-- When using Program (refl_equal and Vnil have maximal implicit
-  arguments, lemmas about measure have a different form, ...).
+- 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). [Automata]
+  (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. [CoLoR]
+  meaningless part of them.
 
 - When rewriting using setoid equality, the default equality found
-  might be different. [CoRN]
+  might be different.