summaryrefslogtreecommitdiff
path: root/CHANGES
blob: b094d8ffba66cf007bb514d85863baaeb8f65308 (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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
Changes from V8.0
=================

Syntax

- No more support for version 7 syntax and for translation to version 8 syntax.
- Support for primitive interpretation of string literals
- Extended support for Unicode ranges (Unicode doc TODO)

Environment variables

- COQREMOTEBROWSER to set the command invoked to start the remote browser
  both in Coq and coqide. Standard syntax: "%s" is the placeholder for the
  URL (doc TODO)

Vernacular commands

- Added "Print Ltac qualid" to print a user defined tactic (doc TODO)
- Added "Print Rewrite HintDb" to print the content of a DB used by
  autorewrite (doc TODO)
- Added "Print Canonical Projections" (doc TODO)
- Added "Example" as synonym of "Definition"
- Added "Property", "Proposition" and "Corollary" as extra synonyms of "Lemma"

Gallina

- Added disjunctive patterns in match-with patterns

Ltac

- New primitive "external" for communication with tool external to Coq
- Semantics of "match t with" changed: if a clause returns a
  tactic, it is now applied to the current goal. If it fails, the next
  clause or next matching subterm is tried (i.e. it behaves as "match
  goal with").
- New modifier "lazy" (TODO) for "match t with" and "match goal with" telling
  to delay the evaluation of tactic expression.
- Hint base name can be parametric in auto and trivial.

Tactics

- New implementation and generalization of [setoid_]* (setoid_rewrite,
  setoid_symmetry, setoid_transitivity, setoid_reflexivity and autorewite).
  New syntax for declaring relations and morphisms (old syntax still working
  with minor modifications, but deprecated) (doc TODO)
- Added "clear - id" to clear all hypotheses except the ones depending in id.
- Added "dependent rewrite term" and "dependent rewrite term in hyp" (doc TODO)
- The argument of Declare Left Step and Declare Right Step is now a term
  (it used to be a reference) (doc TODO)
- Omega now handles arbitrary precision integers
- Idtac can now be left implicit in a [...|...] construct: for instance, 
  [ foo | | bar ] stands for [ foo | idtac | bar ]. (doc TODO). 
- "Tactic Notation" extended to allow notations of tacticals (doc TODO).
- Added "autorewrite with ... in hyp [using ...]" (doc TODO).
- Added entry constr_may_eval for tactic extensions (new syntax).
- Fixed a "fold" bug (non critical and possible source of incompatibilities).
- Added classical_left and classical_right which transforms |- A \/ B into 
  ~B |- A and ~A |- B respectively.
- Added command "Declare Implicit Tactic" to set up a default tactic to be
  used to solve unresolved subterms of term arguments of tactics.
- Better support for coercions to Sortclass in tactics expecting type arguments
- Low-priority term printer made available in ML-written tactic extensions
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns
- New introduction pattern "?" for letting Coq choose a name
- Added "eassumption"
- Added option 'using lemmas' to auto, trivial and eauto
- Numbering of "pattern", "unfold", "simpl", ... occurrences in "match
  with" made consistent with the printing of the return clause after
  the term to match in the "match-with" construct (use "Set Printing All"
  to see hidden occurrences).
- New definition command: "GenFixpoint" (TODO) (doc)
- functional induction has been re-implemented from the new definition
  command (doc TODO)
- Genralisation of induction "induction x1...xn using scheme" where
  scheme is an induction principle with complex predicates (like the
  ones generated by function induction) (doc TODO).


Modules

- Added "Locate Module qualid" to get the full path of a module.
- Module/Declare Module syntax made more uniform (doc TODO)
- Added syntactic sugar "Declare Module Export/Import" and
  "Module Export/Import" (doc TODO)
- Added syntactic sugar "Module M(Export/Import X Y: T)" and
  "Module Type M(Export/Import X Y: T)"
  (only for interactive definitions) (doc TODO)
- Construct "with" generalized to module paths:
   T with (Definition|Module) M1.M2....Mn.l := l'.  (doc TODO)

Notations

- "format" option aware of recursive notations.
- added insertion of spaces by default in recursive notations w/o separators.
- no more automatic printing box in case of user-provided printing "format".
- new notation "exists! x:A, P" for unique existence.

Library

- Small extension of Zmin.V, new Zmax.v, new Zminmax.v
- New library on String and Ascii characters (contributed by L. Thery)
- Few other improvements in ZArith potentially exceptionally breaking the
  compatibility (useless hypothesys of Zgt_square_simpl and
  Zlt_square_simpl removed; fixed names mentioning letter O instead of
  digit 0; weaken premises in Z_lt_induction)
- More lemmas stated on Type in Wf.v, removal of redundant Fix_F
- Coq.List.In_dec has been set transparent (this may exceptionally break
  proof scripts, set it locally opaque for compatibility)
- Change of the internal names of lemmas in OmegaLemmas

Tools

- New semantics for coqtop options ("-batch" expects option "-top dir"
  for loading vernac file that contains definitions).
- coq_makefile now removes custom targets that are file names in "make clean"

Changes from V8.0beta to V8.0
=============================

Vernacular commands

- New option "Set Printing All" to deactivate all high-level forms of
  printing (implicit arguments, coercions, destructing let,
  if-then-else, notations, projections)
- "Functional Scheme" and "Functional Induction" extended to polymorphic
  types and dependent types
- Notation now allows recursive patterns, hence recovering parts of the
  fonctionalities of pre-V8 Grammar/Syntax commands
- Command "Print." discontinued.
- Redundant syntax "Implicit Arguments On/Off" discontinued

New syntax

- Semantics change of the if-then-else construction in new syntax: 
  "if c then t1 else t2" now stands for
  "match c with c1 _ ... _ => t1 | c2 _ ... _ => t2 end"
  with no dependency of t1 and t2 in the arguments of the constructors;
  this may cause incompatibilities for files translated using coq 8.0beta

Interpretation scopes

- Delimiting key %bool for bool_scope added
- Import no more needed to activate argument scopes from a module

Tactics and the tactic Language

- Semantics of "assert" is now consistent with the reference manual
- New tactics stepl and stepr for chaining transitivity steps
- Tactic "replace ... with ... in" added
- Intro patterns now supported in Ltac (parsed with prefix "ipattern:")

Executables and tools

- Added option -top to change the name of the toplevel module "Top"
- Coqdoc updated to new syntax and now part of Coq sources
- XML exportation tool now exports the structure of vernacular files 
  (cf chapter 13 in the reference manual)

User contributions

- User contributions have been updated to the new syntax

Bug fixes

- Many bugs have been fixed (cf coq-bugs web page)

Changes from V8.0beta old syntax to V8.0beta
============================================

New concrete syntax

- A completely new syntax for terms
- A more uniform syntax for tactics and the tactic language 
- A few syntactic changes for vernacular commands
- A smart automatic translator translating V8.0 files in old syntax to
  files valid for V8.0

Syntax extensions

- "Grammar" for terms disappears
- "Grammar" for tactics becomes "Tactic Notation"
- "Syntax" disappears
- Introduction of a notion of interpretation scope allowing to use the
  same notations in various contexts without using specific delimiters
  (e.g the same expression "4<=3+x" is interpreted either in "nat",
  "positive", "N" (previously "entier"), "Z", "R", depending on which
  interpretation scope is currently open) [see documentation for details]
- Notation now mandatorily requires a precedence and associativity
  (default was to set precedence to 1 and associativity to none)

Revision of the standard library

- Many lemmas and definitions names have been made more uniform mostly 
  in Arith, NArith, ZArith and Reals (e.g : "times" -> "Pmult",
  "times_sym" -> "Pmult_comm", "Zle_Zmult_pos_right" ->
  "Zmult_le_compat_r", "SUPERIEUR" -> "Gt", "ZERO" -> "Z0")
- Order and names of arguments of basic lemmas on nat, Z, positive and R
  have been made uniform.
- Notions of Coq initial state are declared with (strict) implicit arguments
- eq merged with eqT: old eq disappear, new eq (written =) is old eqT
  and new eqT is syntactic sugar for new eq (notation == is an alias
  for = and is written as it, exceptional source of incompatibilities)
- Similarly, ex, ex2, all, identity are merged with exT, exT2, allT, identityT
- Arithmetical notations for nat, positive, N, Z, R, without needing
  any backquote or double-backquotes delimiters.
- In Lists: new concrete notations; argument of nil is now implicit
- All changes in the library are taken in charge by the translator

Semantical changes during translation

- Recursive keyword set by default (and no longer needed) in Tactic Definition
- Set Implicit Arguments is strict by default in new syntax
- reductions in hypotheses of the form "... in H" now apply to the type
  also if H is a local definition
- etc

Gallina

- New syntax of the form "Inductive bool : Set := true, false : bool." for
  enumerated types
- Experimental syntax of the form p.(fst) for record projections
  (activable with option "Set Printing Projections" which is
   recognized by the translator)

Known problems of the automatic translation

- iso-latin-1 characters are no longer supported: move your files to
  7-bits ASCII or unicode before translation (swith to unicode is
  automatically done if a file is loaded and saved again by coqide)
- Renaming in ZArith: incompatibilities in Coq user contribs due to
  merging names INZ, from Reals, and inject_nat.
- Renaming and new lemmas in ZArith: may clash with names used by users
- Restructuration of ZArith: replace requirement of specific modules
  in ZArith by "Require Import ZArith_base" or "Require Import ZArith"
- Some implicit arguments must be made explicit before translation: typically
  for "length nil", the implicit argument of length must be made explicit
- Grammar rules, Infix notations and V7.4 Notations must be updated wrt the
  new scheme for syntactic extensions (see translator documentation)
- Unsafe for annotation Cases when constructors coercions are used or when
  annotations are eta-reduced predicates
 

Changes from V7.4 to V8.0beta old syntax
========================================

Logic

- Set now predicative by default
- New option -impredicative-set to set Set impredicative
- The standard library doesn't need impredicativity of Set and is
  compatible with the classical axioms which contradict Set impredicativity

Syntax for arithmetic

- Notation "=" and "<>" in Z and R are no longer implicitly in Z or R
  (with possible introduction of a coercion), use <Z>...=... or
  <Z>...<>... instead
- Locate applied to a simple string (e.g. "+") searches for all
  notations containing this string

Vernacular commands

- "Declare ML Module" now allows to import .cma files. This avoids to use a
   bunch of "Declare ML Module" statements when using several ML files.
- "Set Printing Width n" added, allows to change the size of width printing
   (TODO : doc).
- "Implicit Variables Type x,y:t" (new syntax: "Implicit Types x y:t")
  assigns default types for binding variables.
- Declarations of Hints and Notation now accept a "Local" flag not to
  be exported outside the current file even if not in section
- "Print Scopes" prints all notations
- New command "About name" for light printing of type, implicit arguments, etc.
- New command "Admitted" to declare incompletely proven statement as axioms
- New keyword "Conjecture" to declare an axiom intended to be provable
- SearchAbout can now search for lemmas referring to more than one constant
  and on substrings of the name of the lemma
- "Print Implicit" displays the implicit arguments of a constant
- Locate now searches for all names having a given suffix
- New command "Functional Scheme" for building an induction principle
  from a function defined by case analysis and fix.

Commands

- new coqtop/coqc option -dont-load-proofs not to load opaque proofs in memory

Implicit arguments

- Inductive in sections declared with implicits now "discharged" with
  implicits (like constants and variables)
- Implicit Arguments flags are now synchronous with reset
- New switch "Unset/Set Printing Implicits" (new syntax: "Unset/Set Printing
  Implicit") to globally control printing of implicits

Grammar extensions

- UTF-8 encoded unicode blocks 0380-03FF (greek letters) and 2100-214F
  (letter-like, including aleph and double N,Z,Q,R) are supported
  identifiers; UTF-8 unicode blocs 2200-22FF (mathematical operators),
  2A00-2AFF (supplemental mathematical operators) 2300-23FF
  (miscellaneous technical, including sqrt symbol), 2600-26FF
  (miscellaneous symbols) 2190-21FF (arrows A) and 2900-297F (arrows B)
  are supported symbols

Library

- New file about the factorial function in Arith
- An additional elimination Acc_iter for Acc, simplier than Acc_rect. 
  This new elimination principle is used for definition well_founded_induction.
- New library NArith on binary natural numbers
- R is now of type Set
- Restructuration in ZArith library
  - "true_sub" used in Zplus now a definition, not a local one (source
  of incompatibilities in proof referring to true_sub, may need extra Unfold)
  - Some lemmas about minus moved from fast_integer to Arith/Minus.v
  (le_minus, lt_mult_left) (theoretical source of incompatibilities)
  - Several lemmas moved from auxiliary.v and zarith_aux.v to
  fast_integer.v (theoretical source of incompatibilities)
  - Variables names of iff_trans changed (source of incompatibilities)
  - ZArith lemmas named OMEGA something or fast_ something, and lemma new_var 
    are now out of ZArith (except OMEGA2)
  - Redundant ZArith lemmas have been renamed: for the following pairs,
  use the second name (Zle_Zmult_right2, Zle_mult_simpl), (OMEGA2,
  Zle_0_plus), (Zplus_assoc_l, Zplus_assoc), (Zmult_one, Zmult_1_n),
  (Zmult_assoc_l, Zmult_assoc), (Zmult_minus_distr, Zmult_Zminus_distr_l)
  (add_un_double_moins_un_xO, is_double_moins_un),
  (Rlt_monotony_rev,Rlt_monotony_contra) (source of incompatibilities)
- Few minor changes (no more implicit arguments in
  Zmult_Zminus_distr_l and Zmult_Zminus_distr_r, lemmas moved from
  Zcomplements to other files) (rare source of incompatibilities)
- New lemmas provided by users added

Tactic language

- Fail tactic now accepts a failure message
- Idtac tactic now accepts a message
- New primitive tactic "FreshId" (new syntax: "fresh") to generate new names
- Debugger prints levels of calls

Tactics

- Replace can now replace proofs also
- Fail levels are now decremented at "Match Context" blocks only and
  if the right-hand-side of "Match term With" are tactics, these
  tactics are never evaluated immediately and do not induce
  backtracking (in contrast with "Match Context")
- Quantified names now avoid global names of the current module (like
  Intro names did) [source of rare incompatibilities: 2 changes in the set of
  user contribs]
- NewDestruct/NewInduction accepts intro patterns as introduction names
- NewDestruct/NewInduction now work for non-inductive type using option "using"
- A NewInduction naming bug for inductive types with functional
  arguments (e.g. the accessibility predicate) has been fixed (source
  of incompatibilities)
- Symmetry now applies to hypotheses too
- Inversion now accept option "as [ ... ]" to name the hypotheses
- Contradiction now looks also for contradictory hypotheses stating ~A and A
  (source of incompatibility)
- "Contradiction c" try to find an hypothesis in context which
  contradicts the type of c
- Ring applies to new library NArith (require file NArithRing)
- Field now works on types in Set
- Auto with reals now try to replace le by ge (Rge_le is no longer an
  immediate hint), resulting in shorter proofs
- Instantiate now works in hyps (syntax : Instantiate in ...)
- Some new tactics : EConstructor, ELeft, Eright, ESplit, EExists
- New tactic "functional induction" to perform case analysis and
  induction following the definition of a function.
- Clear now fails when trying to remove a local definition used by
  a constant appearing in the current goal

Extraction (See details in contrib/extraction/CHANGES)

- The old commands: 	(Recursive) Extraction Module M.
  are now:              (Recursive) Extraction Library M. 
  To use these commands, M should come from a library M.v 
- The other syntax Extraction & Recursive Extraction now accept 
  module names as arguments. 

Bugs

- see coq-bugs server for the complete list of fixed bugs

Miscellaneous

- Implicit parameters of inductive types definition now taken into
  account for infering other implicit arguments

Incompatibilities

- Persistence of true_sub (4 incompatibilities in Coq user contributions)
- Variable names of some constants changed for a better uniformity (2 changes
  in Coq user contributions)
- Naming of quantified names in goal now avoid global names (2 occurrences)
- NewInduction naming for inductive types with functional arguments
  (no incompatibility in Coq user contributions)
- Contradiction now solve more goals (source of 2 incompatibilities)
- Merge of eq and eqT may exceptionally result in subgoals now
  solved automatically
- Redundant pairs of ZArith lemmas may have different names: it may
  cause "Apply/Rewrite with" to fail if using the first name of a pair
  of redundant lemmas (this is solved by renaming the variables bound by
  "with"; 3 incompatibilities in Coq user contribs)
- ML programs referring to constants from fast_integer.v must use 
  "Coqlib.gen_constant_modules Coqlib.zarith_base_modules" instead

Changes from V7.3.1 to V7.4
===========================

Symbolic notations

- Introduction of a notion of scope gathering notations in a consistent set;
  a notation sets has been developped for nat, Z and R (undocumented)
- New command "Notation" for declaring notations simultaneously for
  parsing and printing (see chap 10 of the reference manual)
- Declarations with only implicit arguments now handled (e.g. the
  argument of nil can be set implicit; use !nil to refer to nil
  without arguments)
- "Print Scope sc" and "Locate ntn" allows to know to what expression a 
  notation is bound
- New defensive strategy for printing or not implicit arguments to ensure
  re-type-checkability of the printed term
- In Grammar command, the only predefined non-terminal entries are ident,
  global, constr and pattern (e.g. nvar, numarg disappears); the only
  allowed grammar types are constr and pattern; ast and ast list are no
  longer supported; some incompatibilities in Grammar: when a syntax is a 
  initial segment of an other one,  Grammar does not work, use Notation

Library

- Lemmas in Set from Compare_dec.v (le_lt_dec, ...) and Wf_nat.v
  (lt_wf_rec, ...) are now transparent. This may be source of
  incompatibilities.
- Syntactic Definitions Fst, Snd, Ex, All, Ex2, AllT, ExT, ExT2,
  ProjS1, ProjS2, Error, Value and Except are turned to
  notations. They now must be applied (incompatibilities only in
  unrealistic cases).
- More efficient versions of Zmult and times (30% faster)
- Reals: the library is now divided in 6 parts (Rbase, Rfunctions,
  SeqSeries, Rtrigo, Ranalysis, Integration). New tactics: Sup and
  RCompute. See Reals.v for details.

Modules

- Beta version, see doc chap 2.5 for commands and chap 5 for theory

Language

- Inductive definitions now accept ">" in constructor types to declare
  the corresponding constructor as a coercion.
- Idem for assumptions declarations and constants when the type is mentionned.
- The "Coercion" and "Canonical Structure" keywords now accept the
  same syntax as "Definition", i.e. "hyps :=c (:t)?" or "hyps :t".
- Theorem-like declaration now accepts the syntax "Theorem thm [x:t;...] : u".
- Remark's and Fact's now definitively behave as Theorem and Lemma: when
  sections are closed, the full name of a Remark or a Fact has no longer a
  section part (source of incompatibilities)
- Opaque Local's (i.e. built by tactics and ended by Qed), do not
  survive section closing any longer; as a side-effect, Opaque Local's
  now appear in the local context of proofs; their body is hidden
  though (source of incompatibilities); use one of Remark/Fact/Lemma/Theorem
  instead to simulate the old behaviour of Local (the section part of
  the name is not kept though)

ML tactic and vernacular commands

- "Grammar tactic" and "Grammar vernac" of type "ast" are no longer
  supported (only "Grammar tactic simple_tactic" of type "tactic"
  remains available).
- Concrete syntax for ML written vernacular commands and tactics is
  now declared at ML level using camlp4 macros TACTIC EXTEND et VERNAC
  COMMAND EXTEND.
- "Check n c" now "n:Check c", "Eval n ..." now "n:Eval ..."
- "Proof with T" (* no documentation *)
-  SearchAbout id - prints all theorems which contain id in their type

Tactic definitions

- Static globalisation of identifiers and global references (source of
  incompatibilities, especially, Recursive keyword is required for
  mutually recursive definitions).
- New evaluation semantics: no more partial evaluation at definition time;
  evaluation of all Tactic/Meta Definition, even producing terms, expect
  a proof context to be evaluated (especially "()" is no longer needed).
- Debugger now shows the nesting level and the reasons of failure

Tactics

- Equality tactics (Rewrite, Reflexivity, Symmetry, Transitivity) now
  understand JM equality
- Simpl and Change now apply to subterms also
- "Simpl f" reduces subterms whose head constant is f
- Double Induction now referring to hypotheses like "Intros until"
- "Inversion" now applies also on quantified hypotheses (naming as
  for Intros until)
- NewDestruct now accepts terms with missing hypotheses
- NewDestruct and NewInduction now accept user-provided elimination scheme
- NewDestruct and NewInduction now accept user-provided introduction names
- Omega could solve goals such as ~`x<y` |- `x>=y` but failed when the
  hypothesis was unfolded to `x < y` -> False. This is fixed. In addition,
  it can also recognize 'False' in the hypothesis and use it to solve the
  goal.
- Coercions now handled in "with" bindings
- "Subst x" replaces all ocurrences of x by t in the goal and hypotheses 
   when an hypothesis x=t or x:=t or t=x exists
- Fresh names for Assert and Pose now based on collision-avoiding
  Intro naming strategy (exceptional source of incompatibilities)
- LinearIntuition (* no documentation *)
- Unfold expects a correct evaluable argument
- Clear expects existing hypotheses

Extraction (See details in contrib/extraction/CHANGES and README):

- An experimental Scheme extraction is provided.
- Concerning Ocaml, extracted code is now ensured to always type-check, 
  thanks to automatic inserting of Obj.magic.
- Experimental extraction of Coq new modules to Ocaml modules.

Proof rendering in natural language

- Export of theories to XML for publishing and rendering purposes now
  includes proof-trees (see http://www.cs.unibo.it/helm)

Miscellaneous

- Printing Coercion now used through the standard keywords Set/Add, Test, Print
- "Print Term id" is an alias for "Print id"
- New switch "Unset/Set Printing Symbols" to control printing of
  symbolic notations
- Two new variants of implicit arguments are available
   - "Unset/Set Contextual Implicits" tells to consider implicit also the
     arguments inferable from the context (e.g. for nil or refl_eq)
   - "Unset/Set Strict Implicits" tells to consider implicit only the
     arguments that are inferable in any case (i.e. arguments that occurs
     as argument of rigid constants in the type of the remaining arguments;
     e.g. the witness of an existential is not strict since it can vanish when
     applied to a predicate which does not use its argument)

Incompatibilities

- "Grammar tactic ... : ast" and "Grammar vernac ... : ast" are no
  longer supported, use TACTIC EXTEND and VERNAC COMMAND EXTEND on the
  ML-side instead
- Transparency of le_lt_dec and co (leads to some simplification in
  proofs; in some cases, incompatibilites is solved by declaring locally 
  opaque the relevant constant)
- Opaque Local do not now survive section closing (rename them into
  Remark/Lemma/... to get them still surviving the sections; this
  renaming allows also to solve incompatibilites related to now
  forbidden calls to the tactic Clear)
- Remark and Fact have no longer (very) long names (use Local instead in case
  of name conflict)

Bugs

- Improved localisation of errors in Syntactic Definitions
- Induction principle creation failure in presence of let-in fixed (#238)
- Inversion bugs fixed (#212 and #220)
- Omega bug related to Set fixed (#180)
- Type-checking inefficiency of nested destructuring let-in fixed (#216)
- Improved handling of let-in during holes resolution phase (#239)

Efficiency

- Implementation of a memory sharing strategy reducing memory
  requirements by an average ratio of 3.

Changes from V7.3 to V7.3.1
===========================

Bug fixes

  - Corrupted Field tactic and Match Context tactic construction fixed
  - Checking of names already existing in Assert added (PR#182)
  - Invalid argument bug in Exact tactic solved (PR#183)
  - Colliding bound names bug fixed (PR#202)
  - Wrong non-recursivity test for Record fixed (PR#189)
  - Out of memory/seg fault bug related to parametric inductive fixed (PR#195)
  - Setoid_replace/Setoid_rewrite bug wrt "==" fixed

Misc

  - Ocaml version >= 3.06 is needed to compile Coq from sources
  - Simplification of fresh names creation strategy for Assert, Pose and 
    LetTac (PR#192)

Changes from V7.2 to V7.3
=========================

Language

- Slightly improved compilation of pattern-matching (slight source of
  incompatibilities)
- Record's now accept anonymous fields "_" which does not build projections
- 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)

Tactics

- New tactic "Rename x into y" for renaming hypotheses
- New tactics "Pose x:=u" and "Pose u" to add definitions to local context
- Pattern now working on partially applied subterms
- Ring no longer applies irreversible congruence laws of mult but
  better applies congruence laws of plus (slight source of incompatibilities).
- Field now accepts terms to be simplified as arguments (as for Ring). This
  extension has been also implemented using the toplevel tactic language.
- 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)
- "Match Context" now matching more recent hypotheses first and failing only 
  on user errors and Fail tactic (possible source of incompatibilities)
- Tactic Definition's without arguments now allowed in Coq states
- Better simplification and discrimination made by Inversion (source
  of incompatibilities)

Bugs

- "Intros H" now working like "Intro H" trying first to reduce if not a product
- Forward dependencies in Cases now taken into account
- Known bugs related to Inversion and let-in's fixed
- Bug unexpected Delta with let-in now fixed

Extraction (details in contrib/extraction/CHANGES or documentation)

- Signatures of extracted terms are now mostly expunged from dummy arguments.
- Haskell extraction is now operational (tested & debugged).  

Standard library

- 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
- Peano_dec.v and Compare_dec.v now part of Arith.v

Tools

- 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) 

User Contributions

- CongruenceClosure (congruence closure decision procedure)
  [Pierre Corbineau, ENS Cachan]
- MapleMode (an interface to embed Maple simplification procedures over
  rational fractions in Coq)
  [David Delahaye, Micaela Mayero, Chalmers University]
- Presburger: A formalization of Presburger's algorithm 
  [Laurent Thery, INRIA Sophia Antipolis]
- Chinese has been rewritten using Z from ZArith as datatype
  ZChinese is the new version, Chinese the obsolete one
  [Pierre Letouzey, LRI Orsay]

Incompatibilities

- Ring: exceptional incompatibilities (1 above 650 in submitted user
  contribs, leading to a simplification)
- Intuition: does not unfold any definition except "<->" and "~"
- 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)
- 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
- Inversion: better simplification and discrimination may occasionally
  lead to less subgoals and/or hypotheses and different naming of hypotheses
- Unification done by Apply/Elim has been changed and may exceptionally lead
  to incompatible instantiations
- 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)

Changes from V7.1 to V7.2
=========================

Language

- Automatic insertion of patterns for local definitions in the type of
  the constructors of an inductive types (for compatibility with V6.3
  let-in style)
- Coercions allowed in Cases patterns
- New declaration "Canonical Structure id = t : I" to help resolution of
  equations of the form (proj ?)=a; if proj(e)=a then a is canonically 
  equipped with the remaining fields in e, i.e. ? is instantiated by e

Tactics

- New tactic "ClearBody H" to clear the body of definitions in local context
- New tactic "Assert H := c" for forward reasoning
- Slight improvement in naming strategy for NewInduction/NewDestruct
- Intuition/Tauto do not perform useless unfolding and work up to conversion

Extraction (details in contrib/extraction/CHANGES or documentation)

- Syntax changes: there are no more options inside the extraction commands. 
  New commands for customization and options have been introduced instead. 
- More optimizations on extracted code. 
- Extraction tests are now embedded in 14 user contributions. 

Standard library

- In [Relations], Rstar.v and Newman.v now axiom-free. 
- In [Sets], Integers.v now based on nat
- In [Arith], more lemmas in Min.v, new file Max.v, tail-recursive
  plus and mult added to Plus.v and Mult.v respectively
- New directory [Sorting] with a proof of heapsort (dragged from 6.3.1 lib)
- In [Reals], more lemmas in Rbase.v, new lemmas on square, square root and
  trigonometric functions (R_sqr.v - Rtrigo.v); a complementary approach
  and new theorems about continuity and derivability in Ranalysis.v;  some
  properties in plane geometry such as translation, rotation or similarity
  in Rgeom.v; finite sums and Chasles property in Rsigma.v

Bugs

- Confusion between implicit args of locals and globals of same base name fixed
- Various incompatibilities wrt inference of "?" in V6.3.1 fixed
- Implicits in infix section variables bug fixed
- Known coercions bugs fixed

- Apply "universe anomaly" bug fixed
- NatRing now working
- "Discriminate 1", "Injection 1", "Simplify_eq 1" now working
- NewInduction bugs with let-in and recursively dependent hypotheses fixed
- Syntax [x:=t:T]u now allowed as mentioned in documentation

- Bug with recursive inductive types involving let-in fixed
- Known pattern-matching bugs fixed
- Known Cases elimination predicate bugs fixed
- Improved errors messages for pattern-matching and projections
- Better error messages for ill-typed Cases expressions

Incompatibilities

- New naming strategy for NewInduction/NewDestruct may affect 7.1 compatibility
- Extra parentheses may exceptionally be needed in tactic definitions.
- Coq extensions written in Ocaml need to be updated (see dev/changements.txt
  for a description of the main changes in the interface files of V7.2)
- New behaviour of Intuition/Tauto may exceptionally lead to incompatibilities

----------------------------------------------------------------------------
Changes from V6.3.1 and V7.0 to V7.1
====================================

Notes:

- items followed by (**) are important sources of incompatibilities
- items followed by (*) may exceptionally be sources of incompatibilities
- items followed by (+) have been introduced in version 7.0


Main novelties
==============

References are to Coq V7.1 reference manual

- New primitive let-in construct (see sections 1.2.8 and )
- Long names (see sections 2.6 and 2.7)
- New high-level tactic language (see chapter 10)
- Improved search facilities (see section 5.2)
- New extraction algorithm managing the Type level (see chapter 17)
- New rewriting tactic for arbitrary equalities (see chapter 19)
- New tactic Field to decide equalities on commutative fields (see 7.11)
- New tactic Fourier to solve linear inequalities on reals numbers (see 7.11)
- New tactics for induction/case analysis in "natural" style (see 7.7)
- Deep restructuration of the code (safer, simpler and more efficient)
- Export of theories to XML for publishing and rendering purposes
  (see http://www.cs.unibo.it/helm)


Details of changes
==================

Language: new "let-in" construction
-----------------------------------

- New construction for local definitions (let-in) with syntax [x:=u]t (*)(+)

- Local definitions allowed in Record (a.k.a. record à la Randy Pollack)


Language: long names
--------------------

- Each construction has a unique absolute names built from a base
  name, the name of the module in which they are defined (Top if in
  coqtop), and possibly an arbitrary long sequence of directory (e.g.
  "Coq.Lists.PolyList.flat_map" where "Coq" means that "flat_map" is part
  of Coq standard library, "Lists" means it is defined in the Lists
  library and "PolyList" means it is in the file Polylist) (+)

- Constructions can be referred by their base name, or, in case of
  conflict, by a "qualified" name, where the base name is prefixed
  by the module name (and possibly by a directory name, and so
  on). A fully qualified name is an absolute name which always refer
  to the construction it denotes (to preserve the visibility of
  all constructions, no conflict is allowed for an absolute name) (+)

- Long names are available for modules with the possibility of using
  the directory name as a component of the module full name (with
  option -R to coqtop and coqc, or command Add LoadPath) (+)

- Improved conflict resolution strategy (the Unix PATH model),
  allowing more constructions to be referred just by their base name


Language: miscellaneous
-----------------------

- The names of variables for Record projections _and_ for induction principles
  (e.g. sum_ind) is now based on the first letter of their type (main
  source of incompatibility) (**)(+)

- Most typing errors have now a precise location in the source (+)

- Slightly different mechanism to solve "?" (*)(+)

- More arguments may be considered implicit at section closing (*)(+)

- Bug with identifiers ended by a number greater than 2^30 fixed (+)

- New visibility discipline for Remark, Fact and Local: Remark's and
  Fact's now survive at the end of section, but are only accessible using a
  qualified names as soon as their strength expires; Local's disappear and
  are moved into local definitions for each construction persistent at
  section closing


Language: Cases
---------------

- Cases no longer considers aliases inferable from dependencies in types (*)(+)

- A redundant clause in Cases is now an error (*)


Reduction
---------

- New reduction flags "Zeta" and "Evar" in Eval Compute, for inlining of
  local definitions and instantiation of existential variables

- Delta reduction flag does not perform Zeta and Evar reduction any more (*)

- Constants declared as opaque (using Qed) can no longer become
  transparent (a constant intended to be alternatively opaque and
  transparent must be declared as transparent (using Defined)); a risk
  exists (until next Coq version) that Simpl and Hnf reduces opaque
  constants (*)


New tactics
-----------

- New set of tactics to deal with types equipped with specific
  equalities (a.k.a. Setoids, e.g. nat equipped with eq_nat) [by C. Renard]

- New tactic Assert, similar to Cut but expected to be more user-friendly

- New tactic NewDestruct and NewInduction intended to replace Elim
  and Induction, Case and Destruct in a more user-friendly way (see
  restrictions in the reference manual)

- New tactic ROmega: an experimental alternative (based on reflexion) to Omega
  [by P. Crégut]

- New tactic language Ltac (see reference manual) (+)

- New versions of Tauto and Intuition, fully rewritten in the new Ltac
  language; they run faster and produce more compact proofs; Tauto is
  fully compatible but, in exchange of a better uniformity, Intuition
  is slightly weaker (then use Tauto instead) (**)(+)

- New tactic Field to decide equalities on commutative fields (as a
  special case, it works on real numbers) (+)

- New tactic Fourier to solve linear inequalities on reals numbers
  [by L. Pottier] (+)

- New tactics dedicated to real numbers: DiscrR, SplitRmult, SplitAbsolu (+)


Changes in existing tactics
---------------------------

- Reduction tactics in local definitions apply only to the body

- New syntax of the form "Compute in Type of H." to require a reduction on
  the types of local definitions

- Inversion, Injection, Discriminate, ... apply also on the
  quantified premises of a goal (using the "Intros until" syntax)

- Decompose has been fixed but hypotheses may get different names (*)(+)

- Tauto now manages uniformly hypotheses and conclusions of the form
  "t=t" which all are considered equivalent to "True". Especially,
  Tauto now solves goals of the form "H : ~ t = t |- A".

- The "Let" tactic has been renamed "LetTac" and is now based on the
  primitive "let-in" (+)

- Elim can no longer be used with an elimination schema different from
  the one defined at definition time of the inductive type. To overload
  an elimination schema, use "Elim <hyp> using <name of the new schema>"
  (*)(+)

- Simpl no longer unfolds the recursive calls of a mutually defined 
  fixpoint (*)(+)

- Intro now fails if the hypothesis name already exists (*)(+)

- "Require Prolog" is no longer needed (i.e. it is available by default) (*)(+)

- Unfold now fails on a non unfoldable identifier (*)(+)

- Unfold also applies on definitions of the local context

- AutoRewrite now deals only with the main goal and it is the purpose of
  Hint Rewrite to deal with generated subgoals (+)

- Redundant or incompatible instantiations in Apply ... with ... are now
  correctly managed (+)


Efficiency
----------

- Excessive memory uses specific to V7.0 fixed

- Sizes of .vo files vary a lot compared to V6.3 (from -30% to +300%
  depending on the developments)

- An improved reduction strategy for lazy evaluation

- A more economical mechanism to ensure logical consistency at the Type level;
  warning: this is experimental and may produce "universes" anomalies
  (please report)


Concrete syntax of constructions
--------------------------------

- Only identifiers starting with "_" or a letter, and followed by letters,
  digits, "_" or "'" are allowed (e.g. "$" and "@" are no longer allowed) (*)

- A multiple binder like (a:A)(a,b:(P a))(Q a) is no longer parsed as
  (a:A)(a0:(P a))(b:(P a))(Q a0) but as (a:A)(a0:(P a))(b:(P a0))(Q a0) (*)(+)

- A dedicated syntax has been introduced for Reals (e.g ``3+1/x``) (+)

- Pretty-printing of Infix notations fixed. (+)


Parsing and grammar extension
-----------------------------

- More constraints when writing ast 

  - "{...}" and the macros $LIST, $VAR, etc. now expect a metavariable
    (an identifier starting with $) (*)
  - identifiers should starts with a letter or "_" and be followed
     by letters, digits, "_" or "'" (other characters are still
     supported but it is not advised to use them) (*)(+)

- Entry "command" in "Grammar" and quotations (<<...>> stuff) is
  renamed "constr" as in "Syntax" (+)

- New syntax "[" sentence_1 ... sentence_n"]." to group sentences (useful
  for Time and to write grammar rules abbreviating several commands) (+)

- The default parser for actions in the grammar rules (and for
  patterns in the pretty-printing rules) is now the one associated to
  the grammar (i.e. vernac, tactic or constr); no need then for
  quotations as in <:vernac:<...>>; to return an "ast", the grammar
  must be explicitly typed with tag ": ast" or ": ast list", or if a
  syntax rule, by using <<...>> in the patterns (expression inside
  these angle brackets are parsed as "ast"); for grammars other than
  vernac, tactic or constr, you may explicitly type the action with
  tags ": constr", ": tactic", or ":vernac" (**)(+)

- Interpretation of names in Grammar rule is now based on long names,
  which allows to avoid problems (or sometimes tricks;) related to
  overloaded names (+)


New commands
------------

- New commands "Print XML All", "Show XML Proof", ... to show or
  export theories to XML to be used with Helm's publishing and rendering
  tools (see http://www.cs.unibo.it/helm) (by Claudio Sacerdoti Coen) (+)

- New commands to manually set implicit arguments (+)

  - "Implicits ident." to activate the implicit arguments mode just for ident
  - "Implicits ident [num1 num2 ...]." to explicitly give which
     arguments have to be considered as implicit

- New SearchPattern/SearchRewrite (by Yves Bertot) (+)

- New commands "Debug on"/"Debug off" to activate/deactivate the tactic
  language debugger (+)

- New commands to map physical paths to logical paths (+)
  - Add LoadPath physical_dir as logical_dir
  - Add Rec LoadPath physical_dir as logical_dir


Changes in existing commands
----------------------------

- Generalization of the usage of qualified identifiers in tactics
  and commands about globals, e.g. Decompose, Eval Delta; 
  Hints Unfold, Transparent, Require

- Require synchronous with Reset; Require's scope stops at Section ending (*)

- For a module indirectly loaded by a "Require" but not exported,
  the command "Import module" turns the constructions defined in the
  module accessible by their short name, and activates the Grammar,
  Syntax, Hint, ... declared in the module (+)

- The scope of the "Search" command can be restricted to some modules (+)

- Final dot in command (full stop/period) must be followed by a blank
  (newline, tabulation or whitespace) (+)

- Slight restriction of the syntax for Cbv Delta: if present, option [-myconst]
  must immediately follow the Delta keyword (*)(+)

- SearchIsos currently not supported

- Add ML Path is now implied by Add LoadPath (+)

- New names for the following commands (+)

  AddPath -> Add LoadPath
  Print LoadPath -> Print LoadPath
  DelPath -> Remove LoadPath
  AddRecPath -> Add Rec LoadPath
  Print Path -> Print Coercion Paths

  Implicit Arguments On -> Set Implicit Arguments
  Implicit Arguments Off -> Unset Implicit Arguments

  Begin Silent -> Set Silent
  End Silent -> Unset Silent.


Tools
-----

- coqtop (+)

  - Two executables: coqtop.byte and coqtop.opt (if supported by the platform)
  - coqtop is a link to the more efficient executable (coqtop.opt if present)
  - option -full is obsolete (+)

- do_Makefile renamed into coq_makefile (+)

- New option -R to coqtop and coqc to map a physical directory to a logical
  one (+)

- coqc no longer needs to create a temporary file

- No more warning if no initialization file .coqrc exists


Extraction
----------

- New algorithm for extraction able to deal with "Type" (+)
  (by J.-C. Filliâtre and P. Letouzey)


Standard library
----------------

- New library on maps on integers (IntMap, contributed by Jean Goubault)

- New lemmas about integer numbers [ZArith]

- New lemmas and a "natural" syntax for reals [Reals] (+)

- Exc/Error/Value renamed into Option/Some/None (*)


New user contributions
----------------------

- Constructive complex analysis and the Fundamental Theorem of Algebra [FTA]
  (Herman Geuvers, Freek Wiedijk, Jan Zwanenburg, Randy Pollack,
   Henk Barendregt, Nijmegen)

- A new axiomatization of ZFC set theory [Functions_in_ZFC]
  (C. Simpson, Sophia-Antipolis)

- Basic notions of graph theory [GRAPHS-BASICS] (Jean Duprat, Lyon)

- A library for floating-point numbers [Float] (Laurent Théry, Sylvie Boldo,
  Sophia-Antipolis)

- Formalisation of CTL and TCTL temporal logic [CtlTctl] (Carlos
  Daniel Luna,Montevideo)

- Specification and verification of the Railroad Crossing Problem
  in CTL and TCTL [RailroadCrossing] (Carlos Daniel Luna,Montevideo)

- P-automaton and the ABR algorithm [PAutomata]
  (Christine Paulin, Emmanuel Freund, Orsay)

- Semantics of a subset of the C language [MiniC] 
  (Eduardo Giménez, Emmanuel Ledinot, Suresnes) 

- Correctness proofs of the following imperative algorithms:
  Bresenham line drawing algorithm [Bresenham], Marché's minimal edition
  distance algorithm [Diff] (Jean-Christophe Filliâtre, Orsay)

- Correctness proofs of Buchberger's algorithm [Buchberger] and RSA
  cryptographic algorithm [Rsa] (Laurent Théry, Sophia-Antipolis)

- Correctness proof of Stalmarck tautology checker algorithm
  [Stalmarck] (Laurent Théry, Pierre Letouzey, Sophia-Antipolis)