COMPATIBILITY


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

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

(see also file CHANGES)

Language

- Constants hidding polymorphic inductive types are now polymorphic themselves.
  This may exceptionally affect the naming of introduction hypotheses if such
  an inductive type in Type is used on small types such as Prop or
  Set: the hypothesis names suffix will default to H instead of X.  As
  a matter of fact, it is recommended to systematically name the
  hypotheses that are later refered to in the proof script.

Tactics

- The apply tactic now unfolds the constants if needed to succeed.  As
  a consequence, use of "try apply" or "repeat apply" or "apply" in
  other Ltac potentially backtracking code may behave differently. Use
  "simple apply" instead.

- Add Relation and Add Morphism on polymorphic relations should now be
  declared with Add Parametric Relation and Add Parametric Morphism.

- Some bug fixes may lead to incompatibilities.

Libraries

- Some changes in the library (as mentioned in the CHANGES file) may
  imply the need for local adaptations.

For the main changes in the ML interfaces, see file
dev/doc/changes.txt in the main archive.