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
|
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".
|
