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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
|
Potential sources of incompatibilities between Coq V8.5 and V8.6
----------------------------------------------------------------
Symptom: An obligation generated by Program or an abstracted subproof
has different arguments.
Cause: Set Shrink Abstract and Set Shrink Obligations are on by default
and the subproof does not use the argument.
Remedy:
- Adapt the script.
- Write an explicit lemma to prove the obligation/subproof and use it
instead (compatible with 8.4).
- Unset the option for the program/proof the obligation/subproof originates
from.
Potential sources of incompatibilities between Coq V8.4 and V8.5
----------------------------------------------------------------
* List of typical changes to be done to adapt files from Coq 8.4 *
* to Coq 8.5 when not using compatibility option "-compat 8.4". *
Symptom: "The reference omega was not found in the current environment".
Cause: "Require Omega" does not import the tactic "omega" any more
Possible solutions:
- use "Require Import OmegaTactic" (not compatible with 8.4)
- use "Require Import Omega" (compatible with 8.4)
- add definition "Ltac omega := Coq.omega.Omega.omega."
Symptom: "intuition" cannot solve a goal (not working anymore on non standard connective)
Cause: "intuition" had an accidental non uniform behavior fixed on non standard connectives
Possible solutions:
- use "dintuition" instead; it is stronger than "intuition" and works
uniformly on non standard connectives, such as n-ary conjunctions or disjunctions
(not compatible with 8.4)
- do the script differently
Symptom: The constructor foo (in type bar) expects n arguments.
Cause: parameters must now be given in patterns
Possible solutions:
- use option "Set Asymmetric Patterns" (compatible with 8.4)
- add "_" for the parameters (not compatible with 8.4)
- turn the parameters into implicit arguments (compatible with 8.4)
Symptom: "NPeano.Nat.foo" not existing anymore
Possible solutions:
- use "Nat.foo" instead
Symptom: typing problems with proj1_sig or similar
Cause: coercion from sig to sigT and similar coercions have been
removed so as to make the initial state easier to understand for
beginners
Solution: change proj1_sig into projT1 and similarly (compatible with 8.4)
* Other detailed changes *
(see also file CHANGES)
- options for *coq* compilation (see below for ocaml).
** [-I foo] is now deprecated and will not add directory foo to the
coq load path (only for ocaml, see below). Just replace [-I foo] by
[-Q foo ""] in your project file and re-generate makefile. Or
perform the same operation directly in your makefile if you edit it
by hand.
** Option -R Foo bar is the same in v8.5 than in v8.4 concerning coq
load path.
** Option [-I foo -as bar] is unchanged but discouraged unless you
compile ocaml code. Use -Q foo bar instead.
for more details: file CHANGES or section "Customization at launch
time" of the reference manual.
- Command line options for ocaml Compilation of ocaml code (plugins)
** [-I foo] is *not* deprecated to add foo to the ocaml load path.
** [-I foo -as bar] adds foo to the ocaml load path *and* adds foo to
the coq load path with logical name bar (shortcut for -I foo -Q foo
bar).
for more details: file CHANGES or section "Customization at launch
time" of the reference manual.
- Universe Polymorphism.
- Refinement, unification and tactics are now aware of universes,
resulting in more localized errors. Universe inconsistencies
should no more get raised at Qed time but during the proof.
Unification *always* produces well-typed substitutions, hence
some rare cases of unifications that succeeded while producing
ill-typed terms before will now fail.
- The [change p with c] tactic semantics changed, now typechecking
[c] at each matching occurrence [t] of the pattern [p], and
converting [t] with [c].
- Template polymorphic inductive types: the partial application
of a template polymorphic type (e.g. list) is not polymorphic.
An explicit parameter application (e.g [fun A => list A]) or
[apply (list _)] will result in a polymorphic instance.
- The type inference algorithm now takes opacity of constants into
account. This may have effects on tactics using type inference
(e.g. induction). Extra "Transparent" might have to be added to
revert opacity of constants.
Type classes.
- When writing an Instance foo : Class A := {| proj := t |} (note the
vertical bars), support for typechecking the projections using the
type information and switching to proof mode is no longer available.
Use { } (without the vertical bars) instead.
Tactic abstract.
- Auxiliary lemmas generated by the abstract tactic are removed from
the global environment and inlined in the proof term when a proof
is ended with Qed. The behavior of 8.4 can be obtained by ending
proofs with "Qed exporting" or "Qed exporting ident, .., ident".
Potential sources of incompatibilities between Coq V8.3 and V8.4
----------------------------------------------------------------
(see also file CHANGES)
The main known incompatibilities between 8.3 and 8.4 are consequences
of the following changes:
- The reorganization of the library of numbers:
Several definitions have new names or are defined in modules of
different names, but a special care has been taken to have this
renaming transparent for the user thanks to compatibility notations.
However some definitions have changed, what might require some
adaptations. The most noticeable examples are:
- The "?=" notation which now bind to Pos.compare rather than former
Pcompare (now Pos.compare_cont).
- Changes in names may induce different automatically generated
names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec").
- Z.add has a new definition, hence, applying "simpl" on subterms of
its body might give different results than before.
- BigN.shiftl and BigN.shiftr have reversed arguments order, the
power function in BigN now takes two BigN.
- Other changes in libraries:
- The definition of functions over "vectors" (list of fixed length)
have changed.
- TheoryList.v has been removed.
- Slight changes in tactics:
- Less unfolding of fixpoints when applying destruct or inversion on
a fixpoint hiding an inductive type (add an extra call to simpl to
preserve compatibility).
- Less unexpected local definitions when applying "destruct"
(incompatibilities solvable by adapting name hypotheses).
- Tactic "apply" might succeed more often, e.g. by now solving
pattern-matching of the form ?f x y = g(x,y) (compatibility
ensured by using "Unset Tactic Pattern Unification"), but also
because it supports (full) betaiota (using "simple apply" might
then help).
- Tactic autorewrite does no longer instantiate pre-existing
existential variables.
- Tactic "info" is now available only for auto, eauto and trivial.
- Miscellaneous changes:
- The command "Load" is now atomic for backtracking (use "Unset
Atomic Load" for compatibility).
Incompatibilities beyond 8.4...
- Syntax: "x -> y" has now lower priority than "<->" "A -> B <-> C" is
now "A -> (B <-> C)"
- Tactics: tauto and intuition no longer accidentally destruct binary
connectives or records other than and, or, prod, sum, iff. In most
of cases, dtauto or dintuition, though stronger than 8.3 tauto and
8.3 intuition will provide compatibility.
- "Solve Obligations using" is now "Solve Obligations with".
|
