This repository has been archived by the owner on May 30, 2022. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCOMPATIBILITY
135 lines (98 loc) · 5.27 KB
/
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
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
Potential sources of incompatibilities between Coq V8.4 and V8.5
----------------------------------------------------------------
(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".