blob: 87082c6b8e4765e9a31008973b93fb70667f947f (
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
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
|
<HTML>
<body bgcolor=white>
<BR>
<b><font size=18>Changes from V7.3 to V7.3.1</font></b>
<BR>
<H3>Bug fixes</H3>
<UL>
<LI> Corrupted Field tactic and Match Context tactic construction fixed
<LI> Checking of names already existing in Assert added (PR#182)
<LI> Invalid argument bug in Exact tactic solved (PR#183)
<LI> Colliding bound names bug fixed (PR#202)
<LI> Wrong non-recursivity test for Record fixed (PR#189)
<LI> Out of memory/seg fault bug related to parametric inductive fixed (PR#195)
<LI> Setoid_replace/Setoid_rewrite bug wrt "==" fixed
</UL>
<H3>Miscellaneous</H3>
<UL>
<LI> Ocaml version >= 3.06 is needed to compile Coq from sources
<LI> Simplification of fresh names creation strategy for Assert, Pose and
LetTac (PR#192)
</UL>
<BR>
<b><font size=18>Changes from V7.2 to V7.3</font></b>
<BR>
<H3>Language</H3>
<UL>
<LI> Slightly improved compilation of pattern-matching (slight source of
incompatibilities)
<LI> Record's now accept anonymous fields "_" which does not build projections
<LI> Changes in the allowed elimination sorts for certain class of inductive
definitions : an inductive definition without constructors
of Sort Prop can be eliminated on sorts Set and Type A "singleton"
inductive definition (one constructor with arguments in the sort Prop
like conjunction of two propositions or equality) can be eliminated
directly on sort Type (In V7.2, only the sorts Prop and Set were allowed)
</UL>
<H3>Tactics</H3>
<UL>
<LI> New tactic "Rename x into y" for renaming hypotheses
<LI> New tactics "Pose x:=u" and "Pose u" to add definitions to local context
<LI> Pattern now working on partially applied subterms
<LI> Ring no longer applies irreversible congruence laws of mult but
better applies congruence laws of plus (slight source of incompatibilities).
<LI> Intuition does no longer unfold constants except "<->" and "~". It
can be parameterized by a tactic. It also can introduce dependent
product if needed (source of incompatibilities)
<LI> "Match Context" now matching more recent hypotheses first and failing only
on user errors and Fail tactic (possible source of incompatibilities)
<LI> Tactic Definition's without arguments now allowed in Coq states
<LI> Better simplification and discrimination made by Inversion (source
of incompatibilities)
</UL>
<H3>Bugs</H3>
<UL>
<LI> "Intros H" now working like "Intro H" trying first to reduce if not a product
<LI> Forward dependencies in Cases now taken into account
<LI> Known bugs related to Inversion and let-in's fixed
<LI> Bug unexpected Delta with let-in now fixed
</UL>
<H3>Extraction (details in contrib/extraction/CHANGES or documentation)</H3>
<UL>
<LI> Signatures of extracted terms are now mostly expunged from dummy arguments.
<LI> Haskell extraction is now operational (tested & debugged).
</UL>
<H3>Standard library</H3>
<UL>
<LI> Some additions in [ZArith]: three files (Zcomplements.v, Zpower.v
and Zlogarithms.v) moved from contrib/omega in order to be more
visible, one Zsgn function, more induction principles (Wf_Z.v and
tail of Zcomplements.v), one more general Euclid theorem
<LI> Peano_dec.v and Compare_dec.v now part of Arith.v
</UL>
<H3>Tools</H3>
<UL>
<LI> new option -dump-glob to coqtop to dump globalizations (to be used by the
new documentation tool coqdoc; see http://www.lri.fr/~filliatr/coqdoc)
</UL>
<H3>User Contributions</H3>
<UL>
<LI> CongruenceClosure (congruence closure decision procedure)
<LI> MapleMode (an interface to embed Maple simplification procedures in Coq)
<LI> Presburger (a formalization of Presburger's algorithm as stated in the initial paper by Presburger)
<LI> Chinese has been rewritten using Z from ZArith as datatype
ZChinese is the new version, Chinese the obsolete one
</UL>
<H3>Incompatibilities</H3>
<UL>
<LI> Ring: exceptional incompatibilities (1 above 650 in submitted user
contribs, leading to a simplification)
<LI> Intuition: does not unfold any definition except "<->" and "~"
<LI> Cases: removal of some extra Cases in configurations of the form
"Cases ... of C _ => ... | _ D => ..." (effects on 2 definitions of
submitted user contributions necessitating the removal of now superfluous
proof steps in 3 different proofs)
<LI> Match Context, in case of incompatibilities because of a now non
trapped error (e.g. Not_found or Failure), use instead tactic Fail
to force Match Context trying the next clause
<LI> Inversion: better simplification and discrimination may occasionally
lead to less subgoals and/or hypotheses and different naming of hypotheses
<LI> Unification done by Apply/Elim has been changed and may exceptionally lead
to incompatible instantiations
<LI> Peano_dec.v and Compare_dec.v parts of Arith.v make Auto more
powerful if these files were not already required (1 occurrence of
this in submitted user contribs)
</UL>
<BR><BR>
<HR>
<BR>
<a href="ftp://ftp.inria.fr/INRIA/coq/V7.2/doc/Changes.html">Previous changes (from Coq V7.1 to V7.2)</a>
<BR>
</BODY>
</HTML>
|
