COMPATIBILITY

Potential sources of incompatibilities between Coq V8.2 and V8.3
----------------------------------------------------------------

(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
  moved or removed names around.

- Infix notation "++" has now to be set at level 60.

- When using Program (refl_equal and Vnil have maximal implicit
  arguments, 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.