Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Newer
Older
100644 65 lines (48 sloc) 2.6 kb
3d931ab Credits for 8.4 + resetting COMPATIBILITY file.
herbelin authored
1 Potential sources of incompatibilities between Coq V8.3 and V8.4
870321b A list of incompatibilities
herbelin authored
2 ----------------------------------------------------------------
3
4 (see also file CHANGES)
5
9dc0809 Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.
herbelin authored
6 The main known incompatibilities between 8.3 and 8.4 are consequences
7 of the following changes:
8
9 - The reorganization of the library of numbers:
10
11 Several definitions have new names or are defined in modules of
12 different names, but a special care has been taken to have this
13 renaming transparent for the user thanks to compatibility notations.
14
15 However some definitions have changed, what might require some
16 adaptations. The most noticeable examples are:
17 - The "?=" notation which now bind to Pos.compare rather than former
18 Pcompare (now Pos.compare_cont).
19 - Changes in names may induce different automatically generated
20 names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec").
21 - Z.add has a new definition, hence, applying "simpl" on subterms of
22 its body might give different results than before.
23 - BigN.shiftl and BigN.shiftr have reversed arguments order, the
24 power function in BigN now takes two BigN.
25
26 - Other changes in libraries:
27
28 - The definition of functions over "vectors" (list of fixed length)
29 have changed.
30 - TheoryList.v has been removed.
31
32 - Slight changes in tactics:
33
34 - Less unfolding of fixpoints when applying destruct or inversion on
35 a fixpoint hiding an inductive type (add an extra call to simpl to
36 preserve compatibility).
37 - Less unexpected local definitions when applying "destruct"
38 (incompatibilities solvable by adapting name hypotheses).
39 - Tactic "apply" might succeed more often, e.g. by now solving
40 pattern-matching of the form ?f x y = g(x,y) (compatibility
41 ensured by using "Unset Tactic Pattern Unification"), but also
42 because it supports (full) betaiota (using "simple apply" might
43 then help).
44 - Tactic autorewrite does no longer instantiate pre-existing
45 existential variables.
46 - Tactic "info" is now available only for auto, eauto and trivial.
47
48 - Miscellaneous changes:
49
50 - The command "Load" is now atomic for backtracking (use "Unset
51 Atomic Load" for compatibility).
ab4484f Some extra INCOMPATIBILITIES since 8.4.
herbelin authored
52
53
54 Incompatibilities beyond 8.4...
55
56 - Syntax: "x -> y" has now lower priority than "<->" "A -> B <-> C" is
57 now "A -> (B <-> C)"
58
59 - Tactics: tauto and intuition no longer accidentally destruct binary
60 connectives or records other than and, or, prod, sum, iff. In most
61 of cases, dtauto or dintuition, though stronger than 8.3 tauto and
62 8.3 intuition will provide compatibility.
63
64 - "Solve Obligations using" is now "Solve Obligations with".
Something went wrong with that request. Please try again.