From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- COMPATIBILITY | 50 ++------------------------------------------------ 1 file changed, 2 insertions(+), 48 deletions(-) (limited to 'COMPATIBILITY') 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 -- cgit v1.2.3