blob: 30f5daf8f5b66a2730110401fb87c667831289ca (
plain)
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
67
68
69
70
71
72
|
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 constant [flip] is automatically unfolded in the goals generated by
Add Morphism (incompatibility with 8.2 beta versions).
- 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
- Type Class syntax has completely since the 8.2beta versions. See the
documentation for the updated syntax.
- 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.
|
