blob: bb293baa96685f71356dbfa201b499c5f855c792 (
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
|
Potential sources of incompatibilities between Coq V8.0 and V8.1
----------------------------------------------------------------
(see also file CHANGES)
- Inductive types in Type are now polymorphic over their parameters in
Type. This may 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. As
a matter of fact, it is recommended to systematically name the
hypotheses that are later refered to in the proof script.
- Some bug fixes may lead to incompatibilities. This is e.g. the case
of inversion on Type which failed to rewrite some hypotheses as it
did on Prop/Set.
- Add Morphism for the Prop/iff setoid now requires a proof of
biimplication instead of a proof of implication.
- The order of arguments in compatibility morphisms changed: the
premises and the parameters are now interleaved while the whole
bunch of parameters used to come first.
- A few changes in the library (as mentioned in the CHANGES file) may
imply the need for local adaptations.
- Occurrence numbering order for unfold, pattern, etc changed for the
match construction: occurrences in the return clause now come after
the occurrences in the term matched; this was the opposite before.
- For changes in the ML interfaces, see file dev/doc/changes.txt in
the main archive.
|