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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52

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.

- The default relation chosen by setoid_replace may differ. The
  workaround is to enforce the choice of the setoid relation with the
  "using relation ..." option.

- The ordering of subgoals generated by setoid_rewrite and
  setoid_replace tactics has been changed. Some reordering in the
  proof script may be necessary. You may also use the 'by ...' option
  of setoid_replace and setoid_rewrite.
  
- The definition of Setoid_Theory has changed. When using the
  constructors of the structure, you need to unfold the definitions
  Reflexive, Symmetric, and Transitive.
 
- The names of bound variables of theorems generated by Add Morphism
  differs, which may cause some problems with scripts that do not name
  variable when perform introductions. Changing intros to the
  appropriate intro x x0 ... xn should fix the problem.

- Some bug fixes may lead to incompatibilities (see CHANGES for a detailed
  account).

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.