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
53
54
55
56
57
58
59
60
61
62
63
64
65
66

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

(see also file CHANGES)

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.

- Tactic firstorder "with" and "using" options have their meaning
  swapped for consistency with auto/eauto. The solution is to swap
  the use of these options in call to firstorder.

- Introduction patterns are more strict. In "intros [ ... | ... | ... ] H",
  the names in the brackets are synchronized so that H denotes the same
  hypothesis in every subgoal.

- Application patterns with a meta variable in function position (?X ?Y) now
  match arbitrary applications as expected. Use a nested 
  [match X with (_ _) => fail 1 | _ => ..] to recover the old semantics.

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

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.

Libraries

- Some changes in the library (as mentioned in the CHANGES file) may
  imply the need for local adaptations. This may particularly be the
  case with the move from Set to Type in libraries FSets, SetoidList,
  ListSet, Sorting and Zmisc. In case of trouble it may help to simply
  declare Set as an alias for Type (see file SetIsType).

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