diff options
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 18 |
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. |