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
|
Potential sources of incompatibilities between Coq V8.2 and V8.3
----------------------------------------------------------------
(see also file CHANGES)
The main incompatibilities between 8.2 and 8.3 are the following
- When defining objects using tactics as in "Definition f binders :
type.", the binders are automatically introduced in the context. The
former behavior can be restored by using "Unset Automatic
Introduction" (for local modification) or "Global Unset Automatic
Introduction" (for inheritance through Require).
- For setoid rewriting, Morphism has been renamed into Proper.
In general, most sources of incompatibilities can be avoided by
calling coqtop or coqc with option "-compat 8.2". The sources of
incompatibilities listed below must however be treated manually.
Syntax
- The word "by" is now a keyword and can no longer be used as an identifier.
[Semantics, IEEE754]
Type inference
- Many changes in using classes. [ATBR]
Library
- New identifiers of the library can hide identifiers. This can be
solved by changing the order of Require or by qualifying the
identifier with the name of its module. [Stalmarck]
- Reorganisation of library (esp. FSets, Sorting, Numbers) may have
moved or removed names around. [FundamentalArithmetics, CoLoR,
Icharate, AMM11262, FSets, FingerTree]
- Infix notation "++" has now to be set at level 60. [LinAlg]
- When using Program (refl_equal and Vnil have maximal implicit
arguments, lemmas about measure have a different form, ...).
Tactics
- The synchronization of introduction names and quantified hypotheses
names may exceptionally lead to different names in "induction"
(usually a name with lower index is required). [Automata]
- More checks in some commands (e.g. in Hint) may lead to forbid some
meaningless part of them. [CoLoR]
- When rewriting using setoid equality, the default equality found
might be different. [CoRN]
|
