1
Changes from V8.2 to forthcoming V8.2pl1
2
========================================
6
- Fixing Not_found bug in Theorem with.
7
- Fixing pattern parsing bug #2087.
8
- Fixing name aliases bug #2085 with modules.
9
- Fixing checker bug #2065 with -impredicative-set option.
10
- Complying with 8.1 heuristic when unification returns several solutions.
11
- Add [Print Opaque Dependencies] command to print the assumptions and
12
the opaque constants a definition uses.
13
- Fixing performance issue in Program's type inference when there are
15
- Fixing bug #2093, using Program does not require to import Program.Tactics
16
anymore, it will use [idtac] as the default obligation tactic.
17
- Fix imports when requiring Setoid, to avoid cluttering the context with
18
internal names (possible source of incompatibility, import Morphisms to fix).
19
- Fixing bug #2089, Combined Scheme was not treating parameters correctly.
20
- Fixing Program to use hooks correctly, when called through [Program Coercion]
22
- Fixing manual implicit arguments to always work and remove
23
[Set Manual Implicit Arguments] option (possible source of incompatibility).
24
- Fixing refine to work with typeclasses.
25
- Fixing implementation of [Context] to discharge class instances only on definitions
26
using some of the parameters or the instance itself (possible source of
31
- Fixing correct binding of quantified hypotheses for induction/destruction
33
- Fixing bad parentheses check in "pose (f binders := ...)" syntax.
34
- Fixing unbalanced parenthesis in Ltac debug trace printer.
35
- Fixing missing sort unification check in lemma application (bug #2084).
36
- Fixing "as" clause of "apply in" that was not working in the general case.
37
- Fixing eauto not using external hints with no pattern.
41
- Fixing missing -c option in coq_makefile.
42
- Temporary hack for coqide.byte "double free or corruption" problem.
43
- Added support for code development under Bazaar.
44
- Added support for compilation under Solaris (thanks to Eric Le Lay, #2078).
45
- Parsing fixes and support for parsing regular comments inline in coqdoc,
46
using option -parse-comments (suggestions by B. Pierce).
48
Changes from V8.1 to V8.2
49
=========================
53
- If a fixpoint is not written with an explicit { struct ... }, then
54
all arguments are tried successively (from left to right) until one is
55
found that satisfies the structural decreasing condition.
56
- New experimental typeclass system giving ad-hoc polymorphism and
57
overloading based on dependent records and implicit arguments.
58
- New syntax "let 'pat := b in c" for let-binding using irrefutable patterns.
59
- New syntax "forall {A}, T" for specifying maximally inserted implicit
61
- Sort of Record/Structure, Inductive and CoInductive defaults to Type
63
- Support for optional "where" notation clauses for record fields.
64
- (Co)Inductive types can be defined as records
65
(e.g. "CoInductive stream := { hd : nat; tl : stream }.")
66
- New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent
68
- Support for sort-polymorphism on constants denoting inductive types.
69
- Several evolutions of the module system (handling of module aliases,
70
functorial module types, an Include feature, etc).
71
- Prop now a subtype of Set (predicative and impredicative forms).
72
- Recursive inductive types in Prop with a single constructor of which
73
all arguments are in Prop is now considered to be a singleton
74
type. It consequently supports all eliminations to Prop, Set and Type.
75
As a consequence, Acc_rect has now a more direct proof [possible source
76
of easily fixed incompatibility in case of manual definition of a recursor
77
in a recursive singleton inductive type].
78
- New syntax to do implicit generalization in binders and inside terms.
79
- New tentative syntax for introduction of record objects without mentioning
80
the constructor {| field := body; ... |}, turning missing fields into holes
81
(compatible with refine and Program).
85
- Added option Global to "Arguments Scope" for section surviving.
86
- Added option "Unset Elimination Schemes" to deactivate the automatic
87
generation of elimination schemes.
88
- Modification of the Scheme command so you can ask for the name to be
89
automatically computed (e.g. Scheme Induction for nat Sort Set).
90
- New command "Combined Scheme" to build combined mutual induction
91
principles from existing mutual induction principles.
92
- New command "Scheme Equality" to build a decidable (boolean) equality
93
for simple inductive datatypes and a decision property over this equality
94
(e.g. Scheme Equality for nat).
95
- Added option "Set Equality Scheme" to make automatic the declaration
96
of the boolean equality when possible.
97
- Source of universe inconsistencies now printed when option
98
"Set Printing Universes" is activated.
99
- New option "Set Printing Existential Instances" for making the display of
100
existential variable instances explicit.
101
- Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the
102
"compute"/"cbv" reduction strategy, respectively meaning reduce only, or
103
everything but, the constants id1 ... idn. "lazy" alone or followed by
104
"[id1 ... idn]", and "-[id1 ... idn]" also supported, meaning apply
105
all of beta-iota-zeta-delta, possibly restricting delta.
106
- New command "Strategy" to control the expansion of constants during
107
conversion tests. It generalizes commands Opaque and Transparent by
108
introducing a range of levels. Lower levels are assigned to constants
109
that should be expanded first.
110
- New options Global and Local to Opaque and Transparent.
111
- New command "Print Assumptions" to display all variables, parameters
112
or axioms a theorem or definition relies on.
113
- "Add Rec LoadPath" now provides references to libraries using partially
114
qualified names (this holds also for coqtop/coqc option -R).
115
- SearchAbout supports negated search criteria, reference to logical objects
116
by their notation, and more generally search of subterms.
117
- "Declare ML Module" now allows to import .cmxs files when Coq is
118
compiled in native code with a version of OCaml that supports native
120
- New command "Create HintDb name [discriminated]" to explicitely declare
121
a new hint database and optionaly turn on a discrimination net
122
implementation to index all the lemmas in the database.
123
- New commands "Hint Transparent" and "Hint Opaque" to set the unfolding
124
status of definitions used by auto. This information is taken into account
125
by the discrimination net and the unification algorithm.
126
- "Hint Extern" now takes an optional pattern and applies the given tactic
127
all the time if no pattern is given.
128
- Specific sort constraints on Record now taken into account.
129
- "Print LoadPath" supports a path argument to filter the display.
133
- Several parts of the libraries are now in Type, in particular FSets,
134
SetoidList, ListSet, Sorting, Zmisc. This may induce a few
135
incompatibilities. In case of trouble while fixing existing development,
136
it may help to simply declare Set as an alias for Type (see file
138
- New arithmetical library in theories/Numbers. It contains:
139
* an abstract modular development of natural and integer arithmetics
140
in Numbers/Natural/Abstract and Numbers/Integer/Abstract
141
* an implementation of efficient computational bounded and unbounded
142
integers that can be mapped to processor native arithmetics.
143
See Numbers/Cyclic/Int31 for 31-bit integers and Numbers/Natural/BigN
144
for unbounded natural numbers and Numbers/Integer/BigZ for unbounded
146
* some proofs that both older libraries Arith, ZArith and NArith and
147
newer BigN and BigZ implement the abstract modular development.
148
This allows in particular BigN and BigZ to already come with a
149
large database of basic lemmas and some generic tactics (ring),
150
This library has still an experimental status, as well as the
151
processor-acceleration mechanism, but both its abstract and its
152
concrete parts are already quite usable and could challenge the use
153
of nat, N and Z in actual developments. Moreover, an extension of
154
this framework to rational numbers is ongoing, and an efficient
155
Q structure is already provided (see Numbers/Rational/BigQ), but
156
this part is currently incomplete (no abstract layer and generic
158
- Many changes in FSets/FMaps. In practice, compatibility with earlier
159
version should be fairly good, but some adaptations may be required.
160
* Interfaces of unordered ("weak") and ordered sets have been factorized
161
thanks to new features of Coq modules (in particular Include), see
162
FSetInterface. Same for maps. Hints in these interfaces have been
163
reworked (they are now placed in a "set" database).
164
* To allow full subtyping between weak and ordered sets, a field
165
"eq_dec" has been added to OrderedType. The old version of OrderedType
166
is now called MiniOrderedType and functor MOT_to_OT allow to
167
convert to the new version. The interfaces and implementations
168
of sets now contain also such a "eq_dec" field.
169
* FSetDecide, contributed by Aaron Bohannon, contains a decision
170
procedure allowing to solve basic set-related goals (for instance,
171
is a point in a particular set ?). See FSetProperties for examples.
172
* Functors of properties have been improved, especially the ones about
173
maps, that now propose some induction principles. Some properties
174
of fold need less hypothesis.
175
* More uniformity in implementations of sets and maps: they all use
176
implicit arguments, and no longer export unnecessary scopes (see
178
* Internal parts of the implementations based on AVL have evolved a
179
lot. The main files FSetAVL and FMapAVL are now much more
180
lightweight now. In particular, minor changes in some functions
181
has allowed to fully separate the proofs of operational
182
correctness from the proofs of well-balancing: well-balancing is
183
critical for efficiency, but not anymore for proving that these
184
trees implement our interfaces, hence we have moved these proofs
185
into appendix files FSetFullAVL and FMapFullAVL. Moreover, a few
186
functions like union and compare have been modified in order to be
187
structural yet efficient. The appendix files also contains
188
alternative versions of these few functions, much closer to the
189
initial Ocaml code and written via the Function framework.
190
- Library IntMap, subsumed by FSets/FMaps, has been removed from
191
Coq Standard Library and moved into a user contribution Cachan/IntMap
192
- Better computational behavior of some constants (eq_nat_dec and
193
le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare
194
transparent, ...) (exceptional source of incompatibilities).
195
- Boolean operators moved from module Bool to module Datatypes (may need
196
to rename qualified references in script and force notations || and &&
197
to be at levels 50 and 40 respectively).
198
- The constructors xI and xO of type positive now have postfix notations
199
"~1" and "~0", allowing to write numbers in binary form easily, for instance
200
6 is 1~1~0 and 4*p is p~0~0 (see BinPos.v).
201
- Improvements to NArith (Nminus, Nmin, Nmax), and to QArith (in particular
202
a better power function).
203
- Changes in ZArith: several additional lemmas (used in theories/Numbers),
204
especially in Zdiv, Znumtheory, Zpower. Moreover, many results in
205
Zdiv have been generalized: the divisor may simply be non-null
206
instead of strictly positive (see lemmas with name ending by
207
"_full"). An alternative file ZOdiv proposes a different behavior
208
(the one of Ocaml) when dividing by negative numbers.
209
- Changes in Arith: EqNat and Wf_nat now exported from Arith, some
210
constructions on nat that were outside Arith are now in (e.g. iter_nat).
211
- In SetoidList, eqlistA now expresses that two lists have similar elements
212
at the same position, while the predicate previously called eqlistA
213
is now equivlistA (this one only states that the lists contain the same
214
elements, nothing more).
216
* Most statement in "sigT" (including the
217
completeness axiom) are now in "sig" (in case of incompatibility,
218
use proj1_sig instead of projT1, sig instead of sigT, etc).
219
* More uniform naming scheme (identifiers in French moved to English,
220
consistent use of 0 -- zero -- instead of O -- letter O --, etc).
221
* Lemma on prod_f_SO is now on prod_f_R0.
222
* Useless hypothesis of ln_exists1 dropped.
223
* New Rlogic.v states a few logical properties about R axioms.
224
* RIneq.v extended and made cleaner.
225
- Slight restructuration of the Logic library regarding choice and classical
226
logic. Addition of files providing intuitionistic axiomatizations of
227
descriptions: Epsilon.v, Description.v and IndefiniteDescription.v.
228
- Definition of pred and minus made compatible with the structural
229
decreasing criterion for use in fixpoints.
230
- Files Relations/Rstar.v and Relations/Newman.v moved out to the user
231
contribution repository (contribution CoC_History). New lemmas about
232
transitive closure added and some bound variables renamed (exceptional
233
risk of incompatibilities).
235
Notations, coercions, implicit arguments and type inference
237
- More automation in the inference of the return clause of dependent
238
pattern-matching problems.
239
- Experimental allowance for omission of the clauses easily detectable as
240
impossible in pattern-matching problems.
241
- Improved inference of implicit arguments, now working inside record
243
- New options "Set Maximal Implicit Insertion", "Set Reversible Pattern
244
Implicit", "Set Strongly Strict Implicit" and "Set Printing Implicit
245
Defensive" for controlling inference and use of implicit arguments.
246
- New modifier in "Implicit Arguments" to force an implicit argument to
247
be maximally inserted.
248
- New options Global and Local to "Implicit Arguments" for section
249
surviving or non export outside module.
250
- Level "constr" moved from 9 to 8.
251
- Structure/Record now printed as Record (unless option Printing All is set).
252
- Support for parametric notations defining constants.
253
- Insertion of coercions below product types refrains to unfold
254
constants (possible source of incompatibility).
255
- New support for fix/cofix in notations.
259
- Second-order pattern-matching now working in Ltac "match" clauses
260
(syntax for second-order unification variable is "@?X").
261
- Support for matching on let bindings in match context using syntax
262
"H := body" or "H := body : type".
263
- (?X ?Y) patterns now match any application instead of only unary
264
applications (possible source of incompatibility).
265
- Ltac accepts integer arguments (syntax is "ltac:nnn" for nnn an integer).
266
- The general sequence tactical "expr_0 ; [ expr_1 | ... | expr_n ]"
267
is extended so that at most one expr_i may have the form "expr .."
268
or just "..". Also, n can be different from the number of subgoals
269
generated by expr_0. In this case, the value of expr (or idtac in
270
case of just "..") is applied to the intermediate subgoals to make
271
the number of tactics equal to the number of subgoals.
272
- A name used as the name of the parameter of a lemma (like f in
273
"apply f_equal with (f:=t)") is now interpreted as a ltac variable
274
if such a variable exists (this is a possible source of
275
incompatibility and it can be fixed by renaming the variables of a
276
ltac function into names that do not clash with the lemmas
277
parameter names used in the tactic).
278
- New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression.
279
- "let rec ... in ... " now supported for expressions without explicit
280
parameters; interpretation is lazy to the contrary of "let ... in ...";
281
hence, the "rec" keyword can be used to turn the argument of a
282
"let ... in ..." into a lazy one.
283
- Patterns for hypotheses types in "match goal" are now interpreted in
285
- A bound variable whose name is not used elsewhere now serves as
286
metavariable in "match" and it gets instantiated by an identifier
287
(allow e.g. to extract the name of a statement like "exists x, P x").
288
- New printing of Ltac call trace for better debugging.
289
- The C-zar (formerly know as declarative) proof language is now properly
294
- New tactics "apply -> term", "apply <- term", "apply -> term in
295
ident", "apply <- term in ident" for applying equivalences (iff).
296
- "apply" and "rewrite" now take open terms (terms with undefined existentials)
298
- Slight improvement of the hnf and simpl tactics when applied on
299
expressions with explicit occurrences of match or fix.
300
- New tactics "eapply in", "erewrite", "erewrite in".
301
- New tactics "ediscriminate", "einjection", "esimplify_eq".
302
- Tactics "discriminate", "injection", "simplify_eq" now support any
303
term as argument. Clause "with" is also supported.
304
- Unfoldable references can be given by notation's string rather than by name
306
- The "with" arguments are now typed using informations from the current goal:
307
allows support for coercions and more inference of implicit arguments.
308
- Application of "f_equal"-style lemmas works better.
309
- Tactics elim, case, destruct and induction now support variants eelim,
310
ecase, edestruct and einduction.
311
- Tactics destruct and induction now support the "with" option and the
312
"in" clause option. If the option "in" is used, an equality is added
313
to remember the term to which the induction or case analysis applied
314
(possible source of parsing incompatibilities when destruct or induction is
315
part of a let-in expression in Ltac; extra parentheses are then required).
316
- New support for "as" clause in tactics "apply in" and "eapply in".
317
- Some new intro patterns:
318
* intro pattern "?A" genererates a fresh name based on A.
319
Caveat about a slight loss of compatibility:
320
Some intro patterns don't need space between them. In particular
321
intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it
322
is still legal but equivalent to intros ?a ?b.
323
* intro pattern "(A & ... & Y & Z)" synonym to "(A,....,(Y,Z)))))"
324
for right-associative constructs like /\ or exists.
325
- Several syntax extensions concerning "rewrite":
326
* "rewrite A,B,C" can be used to rewrite A, then B, then C. These rewrites
327
occur only on the first subgoal: in particular, side-conditions of the
328
"rewrite A" are not concerned by the "rewrite B,C".
329
* "rewrite A by tac" allows to apply tac on all side-conditions generated by
331
* "rewrite A at n" allows to select occurrences to rewrite: rewrite only
332
happen at the n-th exact occurrence of the first successful matching of
334
* "rewrite 3 A" or "rewrite 3!A" is equivalent to "rewrite A,A,A".
335
* "rewrite !A" means rewriting A as long as possible (and at least once).
336
* "rewrite 3?A" means rewriting A at most three times.
337
* "rewrite ?A" means rewriting A as long as possible (possibly never).
338
* many of the above extensions can be combined with each other.
339
- Introduction patterns better respect the structure of context in presence of
340
missing or extra names in nested disjunction-conjunction patterns [possible
341
source of rare incompatibilities].
342
- New syntax "rename a into b, c into d" for "rename a into b; rename c into d"
343
- New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]"
344
to do induction-inversion on instantiated inductive families � la BasicElim.
345
- Tactics "apply" and "apply in" now able to reason modulo unfolding of
346
constants (possible source of incompatibility in situations where apply
347
may fail, e.g. as argument of a try or a repeat and in a ltac function);
348
versions that do not unfold are renamed into "simple apply" and
349
"simple apply in" (usable for compatibility or for automation).
350
- Tactics "apply" and "apply in" now able to traverse conjunctions and to
351
select the first matching lemma among the components of the conjunction;
352
tactic "apply" also able to apply lemmas of conclusion an empty type.
353
- Tactic "apply" now supports application of several lemmas in a row.
354
- Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)".
355
- New tactic "instantiate" (without argument).
356
- Tactic firstorder "with" and "using" options have their meaning swapped for
357
consistency with auto/eauto (source of incompatibility).
358
- Tactic "generalize" now supports "at" options to specify occurrences
359
and "as" options to name the quantified hypotheses.
360
- New tactic "specialize H with a" or "specialize (H a)" allows to transform
361
in-place a universally-quantified hypothesis (H : forall x, T x) into its
362
instantiated form (H : T a). Nota: "specialize" was in fact there in earlier
363
versions of Coq, but was undocumented, and had a slightly different behavior.
364
- New tactic "contradict H" can be used to solve any kind of goal as long as
365
the user can provide afterwards a proof of the negation of the hypothesis H.
366
If H is already a negation, say ~T, then a proof of T is asked.
367
If the current goal is a negation, say ~U, then U is saved in H afterwards,
368
hence this new tactic "contradict" extends earlier tactic "swap", which is
370
- Tactics f_equal is now done in ML instead of Ltac: it now works on any
371
equality of functions, regardless of the arity of the function.
372
- New options "before id", "at top", "at bottom" for tactics "move"/"intro".
373
- Some more debug of reflexive omega (romega), and internal clarifications.
374
Moreover, romega now has a variant "romega with *" that can be also used
375
on non-Z goals (nat, N, positive) via a call to a translation tactic named
376
zify (its purpose is to Z-ify your goal...). This zify may also be used
377
independantly of romega.
378
- Tactic "remember" now supports an "in" clause to remember only selected
379
occurrences of a term.
380
- Tactic "pose proof" supports name overwriting in case of specialization of an
382
- Semi-decision tactic "jp" for first-order intuitionistic logic moved to user
383
contributions (subsumed by "firstorder").
387
- Moved useful tactics in theories/Program and documented them.
388
- Add Program.Basics which contains standard definitions for functional
389
programming (id, apply, flip...)
390
- More robust obligation handling, dependent pattern-matching and
391
well-founded definitions.
392
- Program CoFixpoint is accepted, Program Fixpoint uses the new way to infer
393
which argument decreases structurally.
394
- Program Lemma, Axiom etc... now permit to have obligations in the statement
395
iff they can be automatically solved by the default tactic.
396
- Renamed "Obligations Tactic" command to "Obligation Tactic".
397
- New command "Preterm [ of id ]" to see the actual term fed to Coq for
399
- New option "Transparent Obligations" to control the declaration of
400
obligations as transparent or opaque. All obligations are now transparent
401
by default, otherwise the system declares them opaque if possible.
402
- Changed the notations "left" and "right" to "in_left" and "in_right" to hide
403
the proofs in standard disjunctions, to avoid breaking existing scripts when
404
importing Program. Also, put them in program_scope.
408
- New "Class", "Instance" and "Program Instance" commands to define
409
classes and instances documented in the reference manual.
410
- New binding construct "`{Class_1 param_1 .. param_n, Class_2 ...}"
411
for binding type classes, usable everywhere.
412
- New command " Print Classes " and " Print Instances some_class " to
413
print tables for typeclasses.
414
- New default eauto hint database "typeclass_instances" used by the default
415
typeclass instance search tactic.
416
- New theories directory "theories/Classes" for standard typeclasses
417
declarations. Module Classes.RelationClasses is a typeclass port of
418
Relation_Definitions plus a generic development of algebra on
419
n-ary heterogeneous predicates.
423
- Complete (and still experimental) rewrite of the tactic
424
based on typeclasses. The old interface and semantics are
425
almost entirely respected, except:
427
- Import Setoid is now mandatory to be able to call setoid_replace
428
and declare morphisms.
430
- "-->", "++>" and "==>" are now right associative notations
431
declared at level 55 in scope signature_scope.
432
Their introduction may break existing scripts that defined
433
them as notations with different levels.
435
- One can use [Typeclasses Opaque/Transparent [cst]] to indicate
436
that [cst] should not be unfolded during unification for morphism
437
resolution, by default all constants are transparent.
439
- The [setoid_rewrite]'s semantics change when rewriting with
440
a lemma: it can rewrite two different instantiations of the lemma
441
at once. Use [setoid_rewrite H at 1] for (almost) the usual semantics.
442
[setoid_rewrite] will also try to rewrite under binders now, and can
443
succeed on different terms than before. In particular, it will unify under
444
let-bound variables. When called through [rewrite], the semantics are
447
- [Add Morphism term : id] has different semantics when used with
448
parametric morphism: it will try to find a relation on the parameters
449
too. The behavior has also changed with respect to default relations:
450
the most recently declared Setoid/Relation will be used, the documentation
451
explains how to customize this behavior.
453
- Parametric Relation and Morphism are declared differently, using the
454
new [Add Parametric] commands, documented in the manual.
456
- Setoid_Theory is now an alias to Equivalence, scripts building objects
457
of type Setoid_Theory need to unfold (or [red]) the definitions
458
of Reflexive, Symmetric and Transitive in order to get the same goals
459
as before. Scripts which introduced variables explicitely will not break.
461
- The order of subgoals when doing [setoid_rewrite] with side-conditions
462
is now always the same: first the new goal, then the conditions.
464
- New standard library modules Classes.Morphisms declares
465
standard morphisms on refl/sym/trans relations.
466
Classes.Morphisms_Prop declares morphisms on propositional
467
connectives and Classes.Morphisms_Relations on generalized predicate
468
connectives. Classes.Equivalence declares notations and tactics
469
related to equivalences and Classes.SetoidTactics defines the
470
setoid_replace tactics and some support for the "Add *" interface,
471
notably the tactic applied automatically before each "Add Morphism"
474
- User-defined subrelations are supported, as well as higher-order morphisms
475
and rewriting under binders. The tactic is also extensible entirely in Ltac.
476
The documentation has been updated to cover these features.
478
- [setoid_rewrite] and [rewrite] now support the [at] modifier to select
479
occurrences to rewrite, and both use the [setoid_rewrite] code, even when
480
rewriting with leibniz equality if occurrences are specified.
484
- Improved behavior of the Caml extraction of modules: name clashes should
486
- The command Extract Inductive has now a syntax for infix notations. This
487
allows in particular to map Coq lists and pairs onto Caml ones:
488
Extract Inductive list => list [ "[]" "(::)" ].
489
Extract Inductive prod => "(*)" [ "(,)" ].
490
- In pattern matchings, a default pattern "| _ -> ..." is now used whenever
491
possible if several branches are identical. For instance, functions
492
corresponding to decidability of equalities are now linear instead of
494
- A new instruction Extraction Blacklist id1 .. idn allows to prevent filename
495
conflits with existing code, for instance when extracting module List
500
- CoqIDE font defaults to monospace so as indentation to be meaningful.
501
- CoqIDE supports nested goals and any other kind of declaration in the middle
503
- Undoing non-tactic commands in CoqIDE works faster.
504
- New CoqIDE menu for activating display of various implicit informations.
505
- Added the possibility to choose the location of tabs in coqide:
506
(in Edit->Preferences->Misc)
507
- New Open and Save As dialogs in CoqIDE which filter *.v files.
511
- New stand-alone .vo files verifier "coqchk".
512
- Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir".
513
- New coqtop/coqc option -exclude-dir to exclude subdirs for option -R.
514
- The binary "parser" has been renamed to "coq-parser".
517
- Improved coqdoc and dump of globalization information to give more
518
meta-information on identifiers. All categories of Coq definitions are
519
supported, which makes typesetting trivial in the generated documentation.
520
- A "--interpolate" option permits to use typesetting information from the
521
typechecked part of the file to typeset identifiers appearing in Coq escapings
522
inside the documentation.
523
- Better handling of utf8 ("--utf8" option) and respect of spaces in the source.
524
- Support for hyperlinking and indexing developments in the TeX output.
525
- New option "color" of the coqdoc style file to render identifiers using colors.
526
- Additional macros in the TeX ouput allowing to customize indentation and size of
527
empty lines. New environment "coqdoccode" for Coq code.
531
- Coq installation provides enough files so that Ocaml's extensions need not
532
the Coq sources to be compiled (this assumes O'Caml 3.10 and Camlp5).
533
- New commands "Set Whelp Server" and "Set Whelp Getter" to customize the
535
- Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into
536
"Test Printing Let for ref" and "Test Printing If for ref".
537
- An overhauled build system (new Makefiles); see dev/doc/build-system.txt.
538
- Add -browser option to configure script.
539
- Build a shared library for the C part of Coq, and use it by default on
540
non-(Windows or MacOS) systems. Bytecode executables are now pure. The
541
behaviour is configurable with -coqrunbyteflags, -coqtoolsbyteflags and
542
-custom configure options.
543
- Complexity tests can be skipped by setting the environment variable
544
COQTEST_SKIPCOMPLEXITY.
546
Changes from V8.1gamma to V8.1
547
==============================
551
- Many bugs have been fixed (cf coq-bugs web page)
555
- New tactics ring, ring_simplify and new tactic field now able to manage
556
power to a positive integer constant. Tactic ring on Z and R, and
557
field on R manage power (may lead to incompatibilities with V8.1gamma).
558
- Tactic field_simplify now applicable in hypotheses.
559
- New field_simplify_eq for simplifying field equations into ring equations.
560
- Tactics ring, ring_simplify, field, field_simplify and field_simplify_eq
561
all able to apply user-given equations to rewrite monoms on the fly
566
- New file ConstructiveEpsilon.v defining an epsilon operator and
567
proving the axiom of choice constructively for a countable domain
568
and a decidable predicate.
570
Changes from V8.1beta to V8.1gamma
571
==================================
575
- changed parsing precedence of let/in and fun constructions of Ltac:
576
let x := t in e1; e2 is now parsed as let x := t in (e1;e2).
578
Language and commands
580
- Added sort-polymorphism for definitions in Type (but finally abandonned).
581
- Support for implicit arguments in the types of parameters in
582
(co-)fixpoints and (co-)inductive declarations.
583
- Improved type inference: use as much of possible general information.
584
before applying irreversible unification heuristics (allow e.g. to
585
infer the predicate in "(exist _ 0 (refl_equal 0) : {n:nat | n=0 })").
586
- Support for Miller-Pfenning's patterns unification in type synthesis
587
(e.g. can infer P such that P x y = phi(x,y)).
588
- Support for "where" clause in cofixpoint definitions.
589
- New option "Set Printing Universes" for making Type levels explicit.
593
- Improved implementation of the ring and field tactics. For compatibility
594
reasons, the previous tactics are renamed as legacy ring and legacy field,
595
but should be considered as deprecated.
596
- New declarative mathematical proof language.
597
- Support for argument lists of arbitrary length in Tactic Notation.
598
- [rewrite ... in H] now fails if [H] is used either in an hypothesis
600
- The semantics of [rewrite ... in *] has been slightly modified (see doc).
601
- Support for "as" clause in tactic injection.
602
- New forward-reasoning tactic "apply in".
603
- Ltac fresh operator now builds names from a concatenation of its arguments.
604
- New ltac tactic "remember" to abstract over a subterm and keep an equality
605
- Support for Miller-Pfenning's patterns unification in apply/rewrite/...
606
(may lead to few incompatibilities - generally now useless tactic calls).
610
- Fix for notations involving basic "match" expressions.
611
- Numerous other bugs solved (a few fixes may lead to incompatibilities).
614
Changes from V8.0 to V8.1beta
615
=============================
619
- Added sort-polymorphism on inductive families
620
- Allowance for recursively non uniform parameters in inductive types
624
- No more support for version 7 syntax and for translation to version 8 syntax.
625
- In fixpoints, the { struct ... } annotation is not mandatory any more when
626
only one of the arguments has an inductive type
627
- Added disjunctive patterns in match-with patterns
628
- Support for primitive interpretation of string literals
629
- Extended support for Unicode ranges
633
- Added "Print Ltac qualid" to print a user defined tactic.
634
- Added "Print Rewrite HintDb" to print the content of a DB used by
636
- Added "Print Canonical Projections".
637
- Added "Example" as synonym of "Definition".
638
- Added "Proposition" and "Corollary" as extra synonyms of "Lemma".
639
- New command "Whelp" to send requests to the Helm database of proofs
640
formalized in the Calculus of Inductive Constructions.
641
- Command "functional induction" has been re-implemented from the new
644
Ltac and tactic syntactic extensions
646
- New primitive "external" for communication with tool external to Coq
647
- New semantics for "match t with": if a clause returns a
648
tactic, it is now applied to the current goal. If it fails, the next
649
clause or next matching subterm is tried (i.e. it behaves as "match
650
goal with" does). The keyword "lazymatch" can be used to delay the
651
evaluation of tactics occurring in matching clauses.
652
- Hint base names can be parametric in auto and trivial.
653
- Occurrence values can be parametric in unfold, pattern, etc.
654
- Added entry constr_may_eval for tactic extensions.
655
- Low-priority term printer made available in ML-written tactic extensions.
656
- "Tactic Notation" extended to allow notations of tacticals.
660
- New implementation and generalization of [setoid_]* (setoid_rewrite,
661
setoid_symmetry, setoid_transitivity, setoid_reflexivity and autorewite).
662
New syntax for declaring relations and morphisms (old syntax still working
663
with minor modifications, but deprecated).
664
- New implementation (still experimental) of the ring tactic with a built-in
665
notion of coefficients and a better usage of setoids.
666
- New conversion tactic "vm_compute": evaluates the goal (or an hypothesis)
667
with a call-by-value strategy, using the compiled version of terms.
668
- When rewriting H where H is not directly a Coq equality, search first H for
669
a registered setoid equality before starting to reduce in H. This is unlikely
670
to break any script. Should this happen nonetheless, one can insert manually
671
some "unfold ... in H" before rewriting.
672
- Fixed various bugs about (setoid) rewrite ... in ... (in particular #1101)
673
- "rewrite ... in" now accepts a clause as place where to rewrite instead of
674
juste a simple hypothesis name. For instance:
675
rewrite H in H1,H2 |- * means rewrite H in H1; rewrite H in H2; rewrite H
676
rewrite H in * |- will do try rewrite H in Hi for all hypothesis Hi <> H.
677
- Added "dependent rewrite term" and "dependent rewrite term in hyp".
678
- Added "autorewrite with ... in hyp [using ...]".
679
- Tactic "replace" now accepts a "by" tactic clause.
680
- Added "clear - id" to clear all hypotheses except the ones depending in id.
681
- The argument of Declare Left Step and Declare Right Step is now a term
682
(it used to be a reference).
683
- Omega now handles arbitrary precision integers.
684
- Several bug fixes in Reflexive Omega (romega).
685
- Idtac can now be left implicit in a [...|...] construct: for instance,
686
[ foo | | bar ] stands for [ foo | idtac | bar ].
687
- Fixed a "fold" bug (non critical but possible source of incompatibilities).
688
- Added classical_left and classical_right which transforms |- A \/ B into
689
~B |- A and ~A |- B respectively.
690
- Added command "Declare Implicit Tactic" to set up a default tactic to be
691
used to solve unresolved subterms of term arguments of tactics.
692
- Better support for coercions to Sortclass in tactics expecting type
694
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses.
695
- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns.
696
- New introduction pattern "?" for letting Coq choose a name.
697
- Introduction patterns now support side hypotheses (e.g. intros [|] on
698
"(nat -> nat) -> nat" works).
699
- New introduction patterns "->" and "<-" for immediate rewriting of
700
introduced hypotheses.
701
- Introduction patterns coming after non trivial introduction patterns now
702
force full introduction of the first pattern (e.g. "intros [[|] p]" on
703
"nat->nat->nat" now behaves like "intros [[|?] p]")
704
- Added "eassumption".
705
- Added option 'using lemmas' to auto, trivial and eauto.
706
- Tactic "congruence" is now complete for its intended scope (ground
707
equalities and inequalities with constructors). Furthermore, it
708
tries to equates goal and hypotheses.
709
- New tactic "rtauto" solves pure propositional logic and gives a
710
reflective version of the available proof.
711
- Numbering of "pattern", "unfold", "simpl", ... occurrences in "match
712
with" made consistent with the printing of the return clause after
713
the term to match in the "match-with" construct (use "Set Printing All"
714
to see hidden occurrences).
715
- Generalization of induction "induction x1...xn using scheme" where
716
scheme is an induction principle with complex predicates (like the
717
ones generated by function induction).
718
- Some small Ltac tactics has been added to the standard library
720
* f_equal : instead of using the different f_equalX lemmas
721
* case_eq : a "case" without loss of information. An equality
722
stating the current situation is generated in every sub-cases.
723
* swap : for a negated goal ~B and a negated hypothesis H:~A,
724
swap H asks you to prove A from hypothesis B
725
* revert : revert H is generalize H; clear H.
729
- All type parts should now disappear instead of sometimes producing _
730
(for instance in Map.empty).
731
- Haskell extraction: types of functions are now printed, better
732
unsafeCoerce mechanism, both for hugs and ghc.
733
- Scheme extraction improved, see http://www.pps.jussieu.fr/~letouzey/scheme.
738
- Added "Locate Module qualid" to get the full path of a module.
739
- Module/Declare Module syntax made more uniform.
740
- Added syntactic sugar "Declare Module Export/Import" and
741
"Module Export/Import".
742
- Added syntactic sugar "Module M(Export/Import X Y: T)" and
743
"Module Type M(Export/Import X Y: T)"
744
(only for interactive definitions)
745
- Construct "with" generalized to module paths:
746
T with (Definition|Module) M1.M2....Mn.l := l'.
750
- Option "format" aware of recursive notations.
751
- Added insertion of spaces by default in recursive notations w/o separators.
752
- No more automatic printing box in case of user-provided printing "format".
753
- New notation "exists! x:A, P" for unique existence.
754
- Notations for specific numerals now compatible with generic notations of
755
numerals (e.g. "1" can be used to denote the unit of a group without
760
- New library on String and Ascii characters (contributed by L. Thery).
761
- New library FSets+FMaps of finite sets and maps.
762
- New library QArith on rational numbers.
763
- Small extension of Zmin.V, new Zmax.v, new Zminmax.v.
764
- Reworking and extension of the files on classical logic and
765
description principles (possible incompatibilities)
766
- Few other improvements in ZArith potentially exceptionally breaking the
767
compatibility (useless hypothesys of Zgt_square_simpl and
768
Zlt_square_simpl removed; fixed names mentioning letter O instead of
769
digit 0; weaken premises in Z_lt_induction).
770
- Restructuration of Eqdep_dec.v and Eqdep.v: more lemmas in Type.
771
- Znumtheory now contains a gcd function that can compute within Coq.
772
- More lemmas stated on Type in Wf.v, removal of redundant Acc_iter and
774
- Change of the internal names of lemmas in OmegaLemmas.
775
- Acc in Wf.v and clos_refl_trans in Relation_Operators.v now rely on
776
the allowance for recursively non uniform parameters (possible
777
source of incompatibilities: explicit pattern-matching on these
778
types may require to remove the occurrence associated to their
779
recursively non uniform parameter).
780
- Coq.List.In_dec has been set transparent (this may exceptionally break
781
proof scripts, set it locally opaque for compatibility).
782
- More on permutations of lists in List.v and Permutation.v.
783
- List.v has been much expanded.
784
- New file SetoidList.v now contains results about lists seen with
785
respect to a setoid equality.
786
- Library NArith has been expanded, mostly with results coming from
787
Intmap (for instance a bitwise xor), plus also a bridge between N and
789
- Intmap has been reorganized. In particular its address type "addr" is
790
now N. User contributions known to use Intmap have been adapted
791
accordingly. If you're using this library please contact us.
792
A wrapper FMapIntMap now presents Intmap as a particular implementation
793
of FMaps. New developments are strongly encouraged to use either this
794
wrapper or any other implementations of FMap instead of using directly
795
this obsolete Intmap.
799
- New semantics for coqtop options ("-batch" expects option "-top dir"
800
for loading vernac file that contains definitions).
801
- Tool coq_makefile now removes custom targets that are file names in
803
- New environment variable COQREMOTEBROWSER to set the command invoked
804
to start the remote browser both in Coq and coqide. Standard syntax:
805
"%s" is the placeholder for the URL.
808
Changes from V8.0beta to V8.0
809
=============================
813
- New option "Set Printing All" to deactivate all high-level forms of
814
printing (implicit arguments, coercions, destructing let,
815
if-then-else, notations, projections)
816
- "Functional Scheme" and "Functional Induction" extended to polymorphic
817
types and dependent types
818
- Notation now allows recursive patterns, hence recovering parts of the
819
fonctionalities of pre-V8 Grammar/Syntax commands
820
- Command "Print." discontinued.
821
- Redundant syntax "Implicit Arguments On/Off" discontinued
825
- Semantics change of the if-then-else construction in new syntax:
826
"if c then t1 else t2" now stands for
827
"match c with c1 _ ... _ => t1 | c2 _ ... _ => t2 end"
828
with no dependency of t1 and t2 in the arguments of the constructors;
829
this may cause incompatibilities for files translated using coq 8.0beta
831
Interpretation scopes
833
- Delimiting key %bool for bool_scope added
834
- Import no more needed to activate argument scopes from a module
836
Tactics and the tactic Language
838
- Semantics of "assert" is now consistent with the reference manual
839
- New tactics stepl and stepr for chaining transitivity steps
840
- Tactic "replace ... with ... in" added
841
- Intro patterns now supported in Ltac (parsed with prefix "ipattern:")
843
Executables and tools
845
- Added option -top to change the name of the toplevel module "Top"
846
- Coqdoc updated to new syntax and now part of Coq sources
847
- XML exportation tool now exports the structure of vernacular files
848
(cf chapter 13 in the reference manual)
852
- User contributions have been updated to the new syntax
856
- Many bugs have been fixed (cf coq-bugs web page)
858
Changes from V8.0beta old syntax to V8.0beta
859
============================================
863
- A completely new syntax for terms
864
- A more uniform syntax for tactics and the tactic language
865
- A few syntactic changes for vernacular commands
866
- A smart automatic translator translating V8.0 files in old syntax to
871
- "Grammar" for terms disappears
872
- "Grammar" for tactics becomes "Tactic Notation"
873
- "Syntax" disappears
874
- Introduction of a notion of interpretation scope allowing to use the
875
same notations in various contexts without using specific delimiters
876
(e.g the same expression "4<=3+x" is interpreted either in "nat",
877
"positive", "N" (previously "entier"), "Z", "R", depending on which
878
interpretation scope is currently open) [see documentation for details]
879
- Notation now mandatorily requires a precedence and associativity
880
(default was to set precedence to 1 and associativity to none)
882
Revision of the standard library
884
- Many lemmas and definitions names have been made more uniform mostly
885
in Arith, NArith, ZArith and Reals (e.g : "times" -> "Pmult",
886
"times_sym" -> "Pmult_comm", "Zle_Zmult_pos_right" ->
887
"Zmult_le_compat_r", "SUPERIEUR" -> "Gt", "ZERO" -> "Z0")
888
- Order and names of arguments of basic lemmas on nat, Z, positive and R
889
have been made uniform.
890
- Notions of Coq initial state are declared with (strict) implicit arguments
891
- eq merged with eqT: old eq disappear, new eq (written =) is old eqT
892
and new eqT is syntactic sugar for new eq (notation == is an alias
893
for = and is written as it, exceptional source of incompatibilities)
894
- Similarly, ex, ex2, all, identity are merged with exT, exT2, allT, identityT
895
- Arithmetical notations for nat, positive, N, Z, R, without needing
896
any backquote or double-backquotes delimiters.
897
- In Lists: new concrete notations; argument of nil is now implicit
898
- All changes in the library are taken in charge by the translator
900
Semantical changes during translation
902
- Recursive keyword set by default (and no longer needed) in Tactic Definition
903
- Set Implicit Arguments is strict by default in new syntax
904
- reductions in hypotheses of the form "... in H" now apply to the type
905
also if H is a local definition
910
- New syntax of the form "Inductive bool : Set := true, false : bool." for
912
- Experimental syntax of the form p.(fst) for record projections
913
(activable with option "Set Printing Projections" which is
914
recognized by the translator)
916
Known problems of the automatic translation
918
- iso-latin-1 characters are no longer supported: move your files to
919
7-bits ASCII or unicode before translation (swith to unicode is
920
automatically done if a file is loaded and saved again by coqide)
921
- Renaming in ZArith: incompatibilities in Coq user contribs due to
922
merging names INZ, from Reals, and inject_nat.
923
- Renaming and new lemmas in ZArith: may clash with names used by users
924
- Restructuration of ZArith: replace requirement of specific modules
925
in ZArith by "Require Import ZArith_base" or "Require Import ZArith"
926
- Some implicit arguments must be made explicit before translation: typically
927
for "length nil", the implicit argument of length must be made explicit
928
- Grammar rules, Infix notations and V7.4 Notations must be updated wrt the
929
new scheme for syntactic extensions (see translator documentation)
930
- Unsafe for annotation Cases when constructors coercions are used or when
931
annotations are eta-reduced predicates
934
Changes from V7.4 to V8.0beta old syntax
935
========================================
939
- Set now predicative by default
940
- New option -impredicative-set to set Set impredicative
941
- The standard library doesn't need impredicativity of Set and is
942
compatible with the classical axioms which contradict Set impredicativity
944
Syntax for arithmetic
946
- Notation "=" and "<>" in Z and R are no longer implicitly in Z or R
947
(with possible introduction of a coercion), use <Z>...=... or
949
- Locate applied to a simple string (e.g. "+") searches for all
950
notations containing this string
954
- "Declare ML Module" now allows to import .cma files. This avoids to use a
955
bunch of "Declare ML Module" statements when using several ML files.
956
- "Set Printing Width n" added, allows to change the size of width printing.
957
- "Implicit Variables Type x,y:t" (new syntax: "Implicit Types x y:t")
958
assigns default types for binding variables.
959
- Declarations of Hints and Notation now accept a "Local" flag not to
960
be exported outside the current file even if not in section
961
- "Print Scopes" prints all notations
962
- New command "About name" for light printing of type, implicit arguments, etc.
963
- New command "Admitted" to declare incompletely proven statement as axioms
964
- New keyword "Conjecture" to declare an axiom intended to be provable
965
- SearchAbout can now search for lemmas referring to more than one constant
966
and on substrings of the name of the lemma
967
- "Print Implicit" displays the implicit arguments of a constant
968
- Locate now searches for all names having a given suffix
969
- New command "Functional Scheme" for building an induction principle
970
from a function defined by case analysis and fix.
974
- new coqtop/coqc option -dont-load-proofs not to load opaque proofs in memory
978
- Inductive in sections declared with implicits now "discharged" with
979
implicits (like constants and variables)
980
- Implicit Arguments flags are now synchronous with reset
981
- New switch "Unset/Set Printing Implicits" (new syntax: "Unset/Set Printing
982
Implicit") to globally control printing of implicits
986
- Many newly supported UTF-8 encoded unicode blocks
987
- Greek letters (0380-03FF), Hebrew letters (U05D0-05EF), letter-like
988
symbols (2100-214F, that includes double N,Z,Q,R), prime
989
signs (from 2080-2089) and characters from many written languages
990
are valid in identifiers
991
- mathematical operators (2200-22FF), supplemental mathematical
992
operators (2A00-2AFF), miscellaneous technical (2300-23FF that
993
includes sqrt symbol), miscellaneous symbols (2600-26FF), arrows
994
(2190-21FF and 2900-297F), invisible mathematical operators (from
995
2080-2089), ... are valid symbols
999
- New file about the factorial function in Arith
1000
- An additional elimination Acc_iter for Acc, simplier than Acc_rect.
1001
This new elimination principle is used for definition well_founded_induction.
1002
- New library NArith on binary natural numbers
1003
- R is now of type Set
1004
- Restructuration in ZArith library
1005
- "true_sub" used in Zplus now a definition, not a local one (source
1006
of incompatibilities in proof referring to true_sub, may need extra Unfold)
1007
- Some lemmas about minus moved from fast_integer to Arith/Minus.v
1008
(le_minus, lt_mult_left) (theoretical source of incompatibilities)
1009
- Several lemmas moved from auxiliary.v and zarith_aux.v to
1010
fast_integer.v (theoretical source of incompatibilities)
1011
- Variables names of iff_trans changed (source of incompatibilities)
1012
- ZArith lemmas named OMEGA something or fast_ something, and lemma new_var
1013
are now out of ZArith (except OMEGA2)
1014
- Redundant ZArith lemmas have been renamed: for the following pairs,
1015
use the second name (Zle_Zmult_right2, Zle_mult_simpl), (OMEGA2,
1016
Zle_0_plus), (Zplus_assoc_l, Zplus_assoc), (Zmult_one, Zmult_1_n),
1017
(Zmult_assoc_l, Zmult_assoc), (Zmult_minus_distr, Zmult_Zminus_distr_l)
1018
(add_un_double_moins_un_xO, is_double_moins_un),
1019
(Rlt_monotony_rev,Rlt_monotony_contra) (source of incompatibilities)
1020
- Few minor changes (no more implicit arguments in
1021
Zmult_Zminus_distr_l and Zmult_Zminus_distr_r, lemmas moved from
1022
Zcomplements to other files) (rare source of incompatibilities)
1023
- New lemmas provided by users added
1027
- Fail tactic now accepts a failure message
1028
- Idtac tactic now accepts a message
1029
- New primitive tactic "FreshId" (new syntax: "fresh") to generate new names
1030
- Debugger prints levels of calls
1034
- Replace can now replace proofs also
1035
- Fail levels are now decremented at "Match Context" blocks only and
1036
if the right-hand-side of "Match term With" are tactics, these
1037
tactics are never evaluated immediately and do not induce
1038
backtracking (in contrast with "Match Context")
1039
- Quantified names now avoid global names of the current module (like
1040
Intro names did) [source of rare incompatibilities: 2 changes in the set of
1042
- NewDestruct/NewInduction accepts intro patterns as introduction names
1043
- NewDestruct/NewInduction now work for non-inductive type using option "using"
1044
- A NewInduction naming bug for inductive types with functional
1045
arguments (e.g. the accessibility predicate) has been fixed (source
1046
of incompatibilities)
1047
- Symmetry now applies to hypotheses too
1048
- Inversion now accept option "as [ ... ]" to name the hypotheses
1049
- Contradiction now looks also for contradictory hypotheses stating ~A and A
1050
(source of incompatibility)
1051
- "Contradiction c" try to find an hypothesis in context which
1052
contradicts the type of c
1053
- Ring applies to new library NArith (require file NArithRing)
1054
- Field now works on types in Set
1055
- Auto with reals now try to replace le by ge (Rge_le is no longer an
1056
immediate hint), resulting in shorter proofs
1057
- Instantiate now works in hyps (syntax : Instantiate in ...)
1058
- Some new tactics : EConstructor, ELeft, Eright, ESplit, EExists
1059
- New tactic "functional induction" to perform case analysis and
1060
induction following the definition of a function.
1061
- Clear now fails when trying to remove a local definition used by
1062
a constant appearing in the current goal
1064
Extraction (See details in contrib/extraction/CHANGES)
1066
- The old commands: (Recursive) Extraction Module M.
1067
are now: (Recursive) Extraction Library M.
1068
To use these commands, M should come from a library M.v
1069
- The other syntax Extraction & Recursive Extraction now accept
1070
module names as arguments.
1074
- see coq-bugs server for the complete list of fixed bugs
1078
- Implicit parameters of inductive types definition now taken into
1079
account for infering other implicit arguments
1083
- Persistence of true_sub (4 incompatibilities in Coq user contributions)
1084
- Variable names of some constants changed for a better uniformity (2 changes
1085
in Coq user contributions)
1086
- Naming of quantified names in goal now avoid global names (2 occurrences)
1087
- NewInduction naming for inductive types with functional arguments
1088
(no incompatibility in Coq user contributions)
1089
- Contradiction now solve more goals (source of 2 incompatibilities)
1090
- Merge of eq and eqT may exceptionally result in subgoals now
1091
solved automatically
1092
- Redundant pairs of ZArith lemmas may have different names: it may
1093
cause "Apply/Rewrite with" to fail if using the first name of a pair
1094
of redundant lemmas (this is solved by renaming the variables bound by
1095
"with"; 3 incompatibilities in Coq user contribs)
1096
- ML programs referring to constants from fast_integer.v must use
1097
"Coqlib.gen_constant_modules Coqlib.zarith_base_modules" instead
1099
Changes from V7.3.1 to V7.4
1100
===========================
1104
- Introduction of a notion of scope gathering notations in a consistent set;
1105
a notation sets has been developped for nat, Z and R (undocumented)
1106
- New command "Notation" for declaring notations simultaneously for
1107
parsing and printing (see chap 10 of the reference manual)
1108
- Declarations with only implicit arguments now handled (e.g. the
1109
argument of nil can be set implicit; use !nil to refer to nil
1111
- "Print Scope sc" and "Locate ntn" allows to know to what expression a
1113
- New defensive strategy for printing or not implicit arguments to ensure
1114
re-type-checkability of the printed term
1115
- In Grammar command, the only predefined non-terminal entries are ident,
1116
global, constr and pattern (e.g. nvar, numarg disappears); the only
1117
allowed grammar types are constr and pattern; ast and ast list are no
1118
longer supported; some incompatibilities in Grammar: when a syntax is a
1119
initial segment of an other one, Grammar does not work, use Notation
1123
- Lemmas in Set from Compare_dec.v (le_lt_dec, ...) and Wf_nat.v
1124
(lt_wf_rec, ...) are now transparent. This may be source of
1126
- Syntactic Definitions Fst, Snd, Ex, All, Ex2, AllT, ExT, ExT2,
1127
ProjS1, ProjS2, Error, Value and Except are turned to
1128
notations. They now must be applied (incompatibilities only in
1130
- More efficient versions of Zmult and times (30% faster)
1131
- Reals: the library is now divided in 6 parts (Rbase, Rfunctions,
1132
SeqSeries, Rtrigo, Ranalysis, Integration). New tactics: Sup and
1133
RCompute. See Reals.v for details.
1137
- Beta version, see doc chap 2.5 for commands and chap 5 for theory
1141
- Inductive definitions now accept ">" in constructor types to declare
1142
the corresponding constructor as a coercion.
1143
- Idem for assumptions declarations and constants when the type is mentionned.
1144
- The "Coercion" and "Canonical Structure" keywords now accept the
1145
same syntax as "Definition", i.e. "hyps :=c (:t)?" or "hyps :t".
1146
- Theorem-like declaration now accepts the syntax "Theorem thm [x:t;...] : u".
1147
- Remark's and Fact's now definitively behave as Theorem and Lemma: when
1148
sections are closed, the full name of a Remark or a Fact has no longer a
1149
section part (source of incompatibilities)
1150
- Opaque Local's (i.e. built by tactics and ended by Qed), do not
1151
survive section closing any longer; as a side-effect, Opaque Local's
1152
now appear in the local context of proofs; their body is hidden
1153
though (source of incompatibilities); use one of Remark/Fact/Lemma/Theorem
1154
instead to simulate the old behaviour of Local (the section part of
1155
the name is not kept though)
1157
ML tactic and vernacular commands
1159
- "Grammar tactic" and "Grammar vernac" of type "ast" are no longer
1160
supported (only "Grammar tactic simple_tactic" of type "tactic"
1162
- Concrete syntax for ML written vernacular commands and tactics is
1163
now declared at ML level using camlp4 macros TACTIC EXTEND et VERNAC
1165
- "Check n c" now "n:Check c", "Eval n ..." now "n:Eval ..."
1166
- "Proof with T" (* no documentation *)
1167
- SearchAbout id - prints all theorems which contain id in their type
1171
- Static globalisation of identifiers and global references (source of
1172
incompatibilities, especially, Recursive keyword is required for
1173
mutually recursive definitions).
1174
- New evaluation semantics: no more partial evaluation at definition time;
1175
evaluation of all Tactic/Meta Definition, even producing terms, expect
1176
a proof context to be evaluated (especially "()" is no longer needed).
1177
- Debugger now shows the nesting level and the reasons of failure
1181
- Equality tactics (Rewrite, Reflexivity, Symmetry, Transitivity) now
1182
understand JM equality
1183
- Simpl and Change now apply to subterms also
1184
- "Simpl f" reduces subterms whose head constant is f
1185
- Double Induction now referring to hypotheses like "Intros until"
1186
- "Inversion" now applies also on quantified hypotheses (naming as
1188
- NewDestruct now accepts terms with missing hypotheses
1189
- NewDestruct and NewInduction now accept user-provided elimination scheme
1190
- NewDestruct and NewInduction now accept user-provided introduction names
1191
- Omega could solve goals such as ~`x<y` |- `x>=y` but failed when the
1192
hypothesis was unfolded to `x < y` -> False. This is fixed. In addition,
1193
it can also recognize 'False' in the hypothesis and use it to solve the
1195
- Coercions now handled in "with" bindings
1196
- "Subst x" replaces all ocurrences of x by t in the goal and hypotheses
1197
when an hypothesis x=t or x:=t or t=x exists
1198
- Fresh names for Assert and Pose now based on collision-avoiding
1199
Intro naming strategy (exceptional source of incompatibilities)
1200
- LinearIntuition (* no documentation *)
1201
- Unfold expects a correct evaluable argument
1202
- Clear expects existing hypotheses
1204
Extraction (See details in contrib/extraction/CHANGES and README):
1206
- An experimental Scheme extraction is provided.
1207
- Concerning Ocaml, extracted code is now ensured to always type-check,
1208
thanks to automatic inserting of Obj.magic.
1209
- Experimental extraction of Coq new modules to Ocaml modules.
1211
Proof rendering in natural language
1213
- Export of theories to XML for publishing and rendering purposes now
1214
includes proof-trees (see http://www.cs.unibo.it/helm)
1218
- Printing Coercion now used through the standard keywords Set/Add, Test, Print
1219
- "Print Term id" is an alias for "Print id"
1220
- New switch "Unset/Set Printing Symbols" to control printing of
1222
- Two new variants of implicit arguments are available
1223
- "Unset/Set Contextual Implicits" tells to consider implicit also the
1224
arguments inferable from the context (e.g. for nil or refl_eq)
1225
- "Unset/Set Strict Implicits" tells to consider implicit only the
1226
arguments that are inferable in any case (i.e. arguments that occurs
1227
as argument of rigid constants in the type of the remaining arguments;
1228
e.g. the witness of an existential is not strict since it can vanish when
1229
applied to a predicate which does not use its argument)
1233
- "Grammar tactic ... : ast" and "Grammar vernac ... : ast" are no
1234
longer supported, use TACTIC EXTEND and VERNAC COMMAND EXTEND on the
1236
- Transparency of le_lt_dec and co (leads to some simplification in
1237
proofs; in some cases, incompatibilites is solved by declaring locally
1238
opaque the relevant constant)
1239
- Opaque Local do not now survive section closing (rename them into
1240
Remark/Lemma/... to get them still surviving the sections; this
1241
renaming allows also to solve incompatibilites related to now
1242
forbidden calls to the tactic Clear)
1243
- Remark and Fact have no longer (very) long names (use Local instead in case
1248
- Improved localisation of errors in Syntactic Definitions
1249
- Induction principle creation failure in presence of let-in fixed (#238)
1250
- Inversion bugs fixed (#212 and #220)
1251
- Omega bug related to Set fixed (#180)
1252
- Type-checking inefficiency of nested destructuring let-in fixed (#216)
1253
- Improved handling of let-in during holes resolution phase (#239)
1257
- Implementation of a memory sharing strategy reducing memory
1258
requirements by an average ratio of 3.
1260
Changes from V7.3 to V7.3.1
1261
===========================
1265
- Corrupted Field tactic and Match Context tactic construction fixed
1266
- Checking of names already existing in Assert added (PR#182)
1267
- Invalid argument bug in Exact tactic solved (PR#183)
1268
- Colliding bound names bug fixed (PR#202)
1269
- Wrong non-recursivity test for Record fixed (PR#189)
1270
- Out of memory/seg fault bug related to parametric inductive fixed (PR#195)
1271
- Setoid_replace/Setoid_rewrite bug wrt "==" fixed
1275
- Ocaml version >= 3.06 is needed to compile Coq from sources
1276
- Simplification of fresh names creation strategy for Assert, Pose and
1279
Changes from V7.2 to V7.3
1280
=========================
1284
- Slightly improved compilation of pattern-matching (slight source of
1286
- Record's now accept anonymous fields "_" which does not build projections
1287
- Changes in the allowed elimination sorts for certain class of inductive
1288
definitions : an inductive definition without constructors
1289
of Sort Prop can be eliminated on sorts Set and Type A "singleton"
1290
inductive definition (one constructor with arguments in the sort Prop
1291
like conjunction of two propositions or equality) can be eliminated
1292
directly on sort Type (In V7.2, only the sorts Prop and Set were allowed)
1296
- New tactic "Rename x into y" for renaming hypotheses
1297
- New tactics "Pose x:=u" and "Pose u" to add definitions to local context
1298
- Pattern now working on partially applied subterms
1299
- Ring no longer applies irreversible congruence laws of mult but
1300
better applies congruence laws of plus (slight source of incompatibilities).
1301
- Field now accepts terms to be simplified as arguments (as for Ring). This
1302
extension has been also implemented using the toplevel tactic language.
1303
- Intuition does no longer unfold constants except "<->" and "~". It
1304
can be parameterized by a tactic. It also can introduce dependent
1305
product if needed (source of incompatibilities)
1306
- "Match Context" now matching more recent hypotheses first and failing only
1307
on user errors and Fail tactic (possible source of incompatibilities)
1308
- Tactic Definition's without arguments now allowed in Coq states
1309
- Better simplification and discrimination made by Inversion (source
1310
of incompatibilities)
1314
- "Intros H" now working like "Intro H" trying first to reduce if not a product
1315
- Forward dependencies in Cases now taken into account
1316
- Known bugs related to Inversion and let-in's fixed
1317
- Bug unexpected Delta with let-in now fixed
1319
Extraction (details in contrib/extraction/CHANGES or documentation)
1321
- Signatures of extracted terms are now mostly expunged from dummy arguments.
1322
- Haskell extraction is now operational (tested & debugged).
1326
- Some additions in [ZArith]: three files (Zcomplements.v, Zpower.v
1327
and Zlogarithms.v) moved from contrib/omega in order to be more
1328
visible, one Zsgn function, more induction principles (Wf_Z.v and
1329
tail of Zcomplements.v), one more general Euclid theorem
1330
- Peano_dec.v and Compare_dec.v now part of Arith.v
1334
- new option -dump-glob to coqtop to dump globalizations (to be used by the
1335
new documentation tool coqdoc; see http://www.lri.fr/~filliatr/coqdoc)
1339
- CongruenceClosure (congruence closure decision procedure)
1340
[Pierre Corbineau, ENS Cachan]
1341
- MapleMode (an interface to embed Maple simplification procedures over
1342
rational fractions in Coq)
1343
[David Delahaye, Micaela Mayero, Chalmers University]
1344
- Presburger: A formalization of Presburger's algorithm
1345
[Laurent Thery, INRIA Sophia Antipolis]
1346
- Chinese has been rewritten using Z from ZArith as datatype
1347
ZChinese is the new version, Chinese the obsolete one
1348
[Pierre Letouzey, LRI Orsay]
1352
- Ring: exceptional incompatibilities (1 above 650 in submitted user
1353
contribs, leading to a simplification)
1354
- Intuition: does not unfold any definition except "<->" and "~"
1355
- Cases: removal of some extra Cases in configurations of the form
1356
"Cases ... of C _ => ... | _ D => ..." (effects on 2 definitions of
1357
submitted user contributions necessitating the removal of now superfluous
1358
proof steps in 3 different proofs)
1359
- Match Context, in case of incompatibilities because of a now non
1360
trapped error (e.g. Not_found or Failure), use instead tactic Fail
1361
to force Match Context trying the next clause
1362
- Inversion: better simplification and discrimination may occasionally
1363
lead to less subgoals and/or hypotheses and different naming of hypotheses
1364
- Unification done by Apply/Elim has been changed and may exceptionally lead
1365
to incompatible instantiations
1366
- Peano_dec.v and Compare_dec.v parts of Arith.v make Auto more
1367
powerful if these files were not already required (1 occurrence of
1368
this in submitted user contribs)
1370
Changes from V7.1 to V7.2
1371
=========================
1375
- Automatic insertion of patterns for local definitions in the type of
1376
the constructors of an inductive types (for compatibility with V6.3
1378
- Coercions allowed in Cases patterns
1379
- New declaration "Canonical Structure id = t : I" to help resolution of
1380
equations of the form (proj ?)=a; if proj(e)=a then a is canonically
1381
equipped with the remaining fields in e, i.e. ? is instantiated by e
1385
- New tactic "ClearBody H" to clear the body of definitions in local context
1386
- New tactic "Assert H := c" for forward reasoning
1387
- Slight improvement in naming strategy for NewInduction/NewDestruct
1388
- Intuition/Tauto do not perform useless unfolding and work up to conversion
1390
Extraction (details in contrib/extraction/CHANGES or documentation)
1392
- Syntax changes: there are no more options inside the extraction commands.
1393
New commands for customization and options have been introduced instead.
1394
- More optimizations on extracted code.
1395
- Extraction tests are now embedded in 14 user contributions.
1399
- In [Relations], Rstar.v and Newman.v now axiom-free.
1400
- In [Sets], Integers.v now based on nat
1401
- In [Arith], more lemmas in Min.v, new file Max.v, tail-recursive
1402
plus and mult added to Plus.v and Mult.v respectively
1403
- New directory [Sorting] with a proof of heapsort (dragged from 6.3.1 lib)
1404
- In [Reals], more lemmas in Rbase.v, new lemmas on square, square root and
1405
trigonometric functions (R_sqr.v - Rtrigo.v); a complementary approach
1406
and new theorems about continuity and derivability in Ranalysis.v; some
1407
properties in plane geometry such as translation, rotation or similarity
1408
in Rgeom.v; finite sums and Chasles property in Rsigma.v
1412
- Confusion between implicit args of locals and globals of same base name fixed
1413
- Various incompatibilities wrt inference of "?" in V6.3.1 fixed
1414
- Implicits in infix section variables bug fixed
1415
- Known coercions bugs fixed
1417
- Apply "universe anomaly" bug fixed
1418
- NatRing now working
1419
- "Discriminate 1", "Injection 1", "Simplify_eq 1" now working
1420
- NewInduction bugs with let-in and recursively dependent hypotheses fixed
1421
- Syntax [x:=t:T]u now allowed as mentioned in documentation
1423
- Bug with recursive inductive types involving let-in fixed
1424
- Known pattern-matching bugs fixed
1425
- Known Cases elimination predicate bugs fixed
1426
- Improved errors messages for pattern-matching and projections
1427
- Better error messages for ill-typed Cases expressions
1431
- New naming strategy for NewInduction/NewDestruct may affect 7.1 compatibility
1432
- Extra parentheses may exceptionally be needed in tactic definitions.
1433
- Coq extensions written in Ocaml need to be updated (see dev/changements.txt
1434
for a description of the main changes in the interface files of V7.2)
1435
- New behaviour of Intuition/Tauto may exceptionally lead to incompatibilities
1437
----------------------------------------------------------------------------
1438
Changes from V6.3.1 and V7.0 to V7.1
1439
====================================
1443
- items followed by (**) are important sources of incompatibilities
1444
- items followed by (*) may exceptionally be sources of incompatibilities
1445
- items followed by (+) have been introduced in version 7.0
1451
References are to Coq V7.1 reference manual
1453
- New primitive let-in construct (see sections 1.2.8 and )
1454
- Long names (see sections 2.6 and 2.7)
1455
- New high-level tactic language (see chapter 10)
1456
- Improved search facilities (see section 5.2)
1457
- New extraction algorithm managing the Type level (see chapter 17)
1458
- New rewriting tactic for arbitrary equalities (see chapter 19)
1459
- New tactic Field to decide equalities on commutative fields (see 7.11)
1460
- New tactic Fourier to solve linear inequalities on reals numbers (see 7.11)
1461
- New tactics for induction/case analysis in "natural" style (see 7.7)
1462
- Deep restructuration of the code (safer, simpler and more efficient)
1463
- Export of theories to XML for publishing and rendering purposes
1464
(see http://www.cs.unibo.it/helm)
1470
Language: new "let-in" construction
1471
-----------------------------------
1473
- New construction for local definitions (let-in) with syntax [x:=u]t (*)(+)
1475
- Local definitions allowed in Record (a.k.a. record � la Randy Pollack)
1478
Language: long names
1479
--------------------
1481
- Each construction has a unique absolute names built from a base
1482
name, the name of the module in which they are defined (Top if in
1483
coqtop), and possibly an arbitrary long sequence of directory (e.g.
1484
"Coq.Lists.PolyList.flat_map" where "Coq" means that "flat_map" is part
1485
of Coq standard library, "Lists" means it is defined in the Lists
1486
library and "PolyList" means it is in the file Polylist) (+)
1488
- Constructions can be referred by their base name, or, in case of
1489
conflict, by a "qualified" name, where the base name is prefixed
1490
by the module name (and possibly by a directory name, and so
1491
on). A fully qualified name is an absolute name which always refer
1492
to the construction it denotes (to preserve the visibility of
1493
all constructions, no conflict is allowed for an absolute name) (+)
1495
- Long names are available for modules with the possibility of using
1496
the directory name as a component of the module full name (with
1497
option -R to coqtop and coqc, or command Add LoadPath) (+)
1499
- Improved conflict resolution strategy (the Unix PATH model),
1500
allowing more constructions to be referred just by their base name
1503
Language: miscellaneous
1504
-----------------------
1506
- The names of variables for Record projections _and_ for induction principles
1507
(e.g. sum_ind) is now based on the first letter of their type (main
1508
source of incompatibility) (**)(+)
1510
- Most typing errors have now a precise location in the source (+)
1512
- Slightly different mechanism to solve "?" (*)(+)
1514
- More arguments may be considered implicit at section closing (*)(+)
1516
- Bug with identifiers ended by a number greater than 2^30 fixed (+)
1518
- New visibility discipline for Remark, Fact and Local: Remark's and
1519
Fact's now survive at the end of section, but are only accessible using a
1520
qualified names as soon as their strength expires; Local's disappear and
1521
are moved into local definitions for each construction persistent at
1528
- Cases no longer considers aliases inferable from dependencies in types (*)(+)
1530
- A redundant clause in Cases is now an error (*)
1536
- New reduction flags "Zeta" and "Evar" in Eval Compute, for inlining of
1537
local definitions and instantiation of existential variables
1539
- Delta reduction flag does not perform Zeta and Evar reduction any more (*)
1541
- Constants declared as opaque (using Qed) can no longer become
1542
transparent (a constant intended to be alternatively opaque and
1543
transparent must be declared as transparent (using Defined)); a risk
1544
exists (until next Coq version) that Simpl and Hnf reduces opaque
1551
- New set of tactics to deal with types equipped with specific
1552
equalities (a.k.a. Setoids, e.g. nat equipped with eq_nat) [by C. Renard]
1554
- New tactic Assert, similar to Cut but expected to be more user-friendly
1556
- New tactic NewDestruct and NewInduction intended to replace Elim
1557
and Induction, Case and Destruct in a more user-friendly way (see
1558
restrictions in the reference manual)
1560
- New tactic ROmega: an experimental alternative (based on reflexion) to Omega
1563
- New tactic language Ltac (see reference manual) (+)
1565
- New versions of Tauto and Intuition, fully rewritten in the new Ltac
1566
language; they run faster and produce more compact proofs; Tauto is
1567
fully compatible but, in exchange of a better uniformity, Intuition
1568
is slightly weaker (then use Tauto instead) (**)(+)
1570
- New tactic Field to decide equalities on commutative fields (as a
1571
special case, it works on real numbers) (+)
1573
- New tactic Fourier to solve linear inequalities on reals numbers
1576
- New tactics dedicated to real numbers: DiscrR, SplitRmult, SplitAbsolu (+)
1579
Changes in existing tactics
1580
---------------------------
1582
- Reduction tactics in local definitions apply only to the body
1584
- New syntax of the form "Compute in Type of H." to require a reduction on
1585
the types of local definitions
1587
- Inversion, Injection, Discriminate, ... apply also on the
1588
quantified premises of a goal (using the "Intros until" syntax)
1590
- Decompose has been fixed but hypotheses may get different names (*)(+)
1592
- Tauto now manages uniformly hypotheses and conclusions of the form
1593
"t=t" which all are considered equivalent to "True". Especially,
1594
Tauto now solves goals of the form "H : ~ t = t |- A".
1596
- The "Let" tactic has been renamed "LetTac" and is now based on the
1597
primitive "let-in" (+)
1599
- Elim can no longer be used with an elimination schema different from
1600
the one defined at definition time of the inductive type. To overload
1601
an elimination schema, use "Elim <hyp> using <name of the new schema>"
1604
- Simpl no longer unfolds the recursive calls of a mutually defined
1607
- Intro now fails if the hypothesis name already exists (*)(+)
1609
- "Require Prolog" is no longer needed (i.e. it is available by default) (*)(+)
1611
- Unfold now fails on a non unfoldable identifier (*)(+)
1613
- Unfold also applies on definitions of the local context
1615
- AutoRewrite now deals only with the main goal and it is the purpose of
1616
Hint Rewrite to deal with generated subgoals (+)
1618
- Redundant or incompatible instantiations in Apply ... with ... are now
1619
correctly managed (+)
1625
- Excessive memory uses specific to V7.0 fixed
1627
- Sizes of .vo files vary a lot compared to V6.3 (from -30% to +300%
1628
depending on the developments)
1630
- An improved reduction strategy for lazy evaluation
1632
- A more economical mechanism to ensure logical consistency at the Type level;
1633
warning: this is experimental and may produce "universes" anomalies
1637
Concrete syntax of constructions
1638
--------------------------------
1640
- Only identifiers starting with "_" or a letter, and followed by letters,
1641
digits, "_" or "'" are allowed (e.g. "$" and "@" are no longer allowed) (*)
1643
- A multiple binder like (a:A)(a,b:(P a))(Q a) is no longer parsed as
1644
(a:A)(a0:(P a))(b:(P a))(Q a0) but as (a:A)(a0:(P a))(b:(P a0))(Q a0) (*)(+)
1646
- A dedicated syntax has been introduced for Reals (e.g ``3+1/x``) (+)
1648
- Pretty-printing of Infix notations fixed. (+)
1651
Parsing and grammar extension
1652
-----------------------------
1654
- More constraints when writing ast
1656
- "{...}" and the macros $LIST, $VAR, etc. now expect a metavariable
1657
(an identifier starting with $) (*)
1658
- identifiers should starts with a letter or "_" and be followed
1659
by letters, digits, "_" or "'" (other characters are still
1660
supported but it is not advised to use them) (*)(+)
1662
- Entry "command" in "Grammar" and quotations (<<...>> stuff) is
1663
renamed "constr" as in "Syntax" (+)
1665
- New syntax "[" sentence_1 ... sentence_n"]." to group sentences (useful
1666
for Time and to write grammar rules abbreviating several commands) (+)
1668
- The default parser for actions in the grammar rules (and for
1669
patterns in the pretty-printing rules) is now the one associated to
1670
the grammar (i.e. vernac, tactic or constr); no need then for
1671
quotations as in <:vernac:<...>>; to return an "ast", the grammar
1672
must be explicitly typed with tag ": ast" or ": ast list", or if a
1673
syntax rule, by using <<...>> in the patterns (expression inside
1674
these angle brackets are parsed as "ast"); for grammars other than
1675
vernac, tactic or constr, you may explicitly type the action with
1676
tags ": constr", ": tactic", or ":vernac" (**)(+)
1678
- Interpretation of names in Grammar rule is now based on long names,
1679
which allows to avoid problems (or sometimes tricks;) related to
1680
overloaded names (+)
1686
- New commands "Print XML All", "Show XML Proof", ... to show or
1687
export theories to XML to be used with Helm's publishing and rendering
1688
tools (see http://www.cs.unibo.it/helm) (by Claudio Sacerdoti Coen) (+)
1690
- New commands to manually set implicit arguments (+)
1692
- "Implicits ident." to activate the implicit arguments mode just for ident
1693
- "Implicits ident [num1 num2 ...]." to explicitly give which
1694
arguments have to be considered as implicit
1696
- New SearchPattern/SearchRewrite (by Yves Bertot) (+)
1698
- New commands "Debug on"/"Debug off" to activate/deactivate the tactic
1699
language debugger (+)
1701
- New commands to map physical paths to logical paths (+)
1702
- Add LoadPath physical_dir as logical_dir
1703
- Add Rec LoadPath physical_dir as logical_dir
1706
Changes in existing commands
1707
----------------------------
1709
- Generalization of the usage of qualified identifiers in tactics
1710
and commands about globals, e.g. Decompose, Eval Delta;
1711
Hints Unfold, Transparent, Require
1713
- Require synchronous with Reset; Require's scope stops at Section ending (*)
1715
- For a module indirectly loaded by a "Require" but not exported,
1716
the command "Import module" turns the constructions defined in the
1717
module accessible by their short name, and activates the Grammar,
1718
Syntax, Hint, ... declared in the module (+)
1720
- The scope of the "Search" command can be restricted to some modules (+)
1722
- Final dot in command (full stop/period) must be followed by a blank
1723
(newline, tabulation or whitespace) (+)
1725
- Slight restriction of the syntax for Cbv Delta: if present, option [-myconst]
1726
must immediately follow the Delta keyword (*)(+)
1728
- SearchIsos currently not supported
1730
- Add ML Path is now implied by Add LoadPath (+)
1732
- New names for the following commands (+)
1734
AddPath -> Add LoadPath
1735
Print LoadPath -> Print LoadPath
1736
DelPath -> Remove LoadPath
1737
AddRecPath -> Add Rec LoadPath
1738
Print Path -> Print Coercion Paths
1740
Implicit Arguments On -> Set Implicit Arguments
1741
Implicit Arguments Off -> Unset Implicit Arguments
1743
Begin Silent -> Set Silent
1744
End Silent -> Unset Silent.
1752
- Two executables: coqtop.byte and coqtop.opt (if supported by the platform)
1753
- coqtop is a link to the more efficient executable (coqtop.opt if present)
1754
- option -full is obsolete (+)
1756
- do_Makefile renamed into coq_makefile (+)
1758
- New option -R to coqtop and coqc to map a physical directory to a logical
1761
- coqc no longer needs to create a temporary file
1763
- No more warning if no initialization file .coqrc exists
1769
- New algorithm for extraction able to deal with "Type" (+)
1770
(by J.-C. Filli�tre and P. Letouzey)
1776
- New library on maps on integers (IntMap, contributed by Jean Goubault)
1778
- New lemmas about integer numbers [ZArith]
1780
- New lemmas and a "natural" syntax for reals [Reals] (+)
1782
- Exc/Error/Value renamed into Option/Some/None (*)
1785
New user contributions
1786
----------------------
1788
- Constructive complex analysis and the Fundamental Theorem of Algebra [FTA]
1789
(Herman Geuvers, Freek Wiedijk, Jan Zwanenburg, Randy Pollack,
1790
Henk Barendregt, Nijmegen)
1792
- A new axiomatization of ZFC set theory [Functions_in_ZFC]
1793
(C. Simpson, Sophia-Antipolis)
1795
- Basic notions of graph theory [GRAPHS-BASICS] (Jean Duprat, Lyon)
1797
- A library for floating-point numbers [Float] (Laurent Th�ry, Sylvie Boldo,
1800
- Formalisation of CTL and TCTL temporal logic [CtlTctl] (Carlos
1801
Daniel Luna,Montevideo)
1803
- Specification and verification of the Railroad Crossing Problem
1804
in CTL and TCTL [RailroadCrossing] (Carlos Daniel Luna,Montevideo)
1806
- P-automaton and the ABR algorithm [PAutomata]
1807
(Christine Paulin, Emmanuel Freund, Orsay)
1809
- Semantics of a subset of the C language [MiniC]
1810
(Eduardo Gim�nez, Emmanuel Ledinot, Suresnes)
1812
- Correctness proofs of the following imperative algorithms:
1813
Bresenham line drawing algorithm [Bresenham], March�'s minimal edition
1814
distance algorithm [Diff] (Jean-Christophe Filli�tre, Orsay)
1816
- Correctness proofs of Buchberger's algorithm [Buchberger] and RSA
1817
cryptographic algorithm [Rsa] (Laurent Th�ry, Sophia-Antipolis)
1819
- Correctness proof of Stalmarck tautology checker algorithm
1820
[Stalmarck] (Laurent Th�ry, Pierre Letouzey, Sophia-Antipolis)
added
removed
CHANGES
