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 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411 1412 1413 1414 1415 1416 1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 1433 1434 1435 1436 1437 1438 1439 1440 1441 1442 1443 1444 1445 1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456 1457 1458 1459 1460 1461 1462 1463 1464 1465 1466 1467 1468 1469 1470 1471 1472 1473 1474 1475 1476 1477 1478 1479 1480 1481 1482 1483 1484 1485 1486 1487 1488 1489 1490 1491 1492 1493 1494 1495 1496 1497 1498 1499 1500 1501 1502 1503 1504 1505 1506 1507 1508 1509 1510 1511 1512 1513 1514 1515 1516 1517 1518 1519 1520 1521 1522 1523 1524 1525 1526 1527 1528 1529 1530 1531 1532 1533 1534 1535 1536 1537 1538 1539 1540 1541 1542 1543 1544 1545 1546 1547 1548 1549 1550 1551 1552 1553 1554 1555 1556 1557 1558 1559 1560 1561 1562 1563 1564 1565 1566 1567 1568 1569 1570 1571 1572 1573 1574 1575 1576 1577 1578 1579 1580 1581 1582 1583 1584 1585 1586 1587 1588 1589 1590 1591 1592 1593 1594 1595 1596 1597 1598 1599 1600 1601 1602 1603 1604 1605 1606 1607 1608 1609 1610 1611 1612 1613 1614 1615 1616 1617 1618 1619 1620 1621 1622 1623 1624 1625 1626 1627 1628 1629 1630 1631 1632 1633 1634 1635 1636 1637 1638 1639 1640 1641 1642 1643 1644 1645 1646 1647 1648 1649 1650 1651 1652 1653 1654 1655 1656 1657 1658 1659 1660 1661 1662 1663 1664 1665 1666 1667 1668 1669 1670 1671 1672 1673 1674 1675 1676 1677 1678 1679 1680 1681 1682 1683 1684 1685 1686 1687 1688 1689 1690 1691 1692 1693 1694 1695 1696 1697 1698 1699 1700 1701 1702 1703 1704 1705 1706 1707 1708 1709 1710 1711 1712 1713 1714 1715 1716 1717 1718 1719 1720 1721 1722 1723 1724 1725 1726 1727 1728 1729 1730 1731 1732 1733 1734 1735 1736 1737 1738 1739 1740 1741 1742 1743 1744 1745 1746 1747 1748 1749 1750 1751 1752 1753 1754 1755 1756 1757 1758 1759 1760 1761 1762 1763 1764 1765 1766 1767 1768 1769 1770 1771 1772 1773 1774 1775 1776 1777 1778 1779 1780 1781 1782 1783 1784 1785 1786 1787 1788 1789 1790 1791 1792 1793 1794 1795 1796 1797 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808 1809 1810 1811 1812 1813 1814 1815 1816 1817 1818 1819 1820

Changes from V8.2 to forthcoming V8.2pl1
========================================
Language and commands
 Fixing Not_found bug in Theorem with.
 Fixing pattern parsing bug #2087.
 Fixing name aliases bug #2085 with modules.
 Fixing checker bug #2065 with impredicativeset option.
 Complying with 8.1 heuristic when unification returns several solutions.
 Add [Print Opaque Dependencies] command to print the assumptions and
the opaque constants a definition uses.
 Fixing performance issue in Program's type inference when there are
many existentials.
 Fixing bug #2093, using Program does not require to import Program.Tactics
anymore, it will use [idtac] as the default obligation tactic.
 Fix imports when requiring Setoid, to avoid cluttering the context with
internal names (possible source of incompatibility, import Morphisms to fix).
 Fixing bug #2089, Combined Scheme was not treating parameters correctly.
 Fixing Program to use hooks correctly, when called through [Program Coercion]
for example.
 Fixing manual implicit arguments to always work and remove
[Set Manual Implicit Arguments] option (possible source of incompatibility).
 Fixing refine to work with typeclasses.
 Fixing implementation of [Context] to discharge class instances only on definitions
using some of the parameters or the instance itself (possible source of
incompatibility).
Tactics
 Fixing correct binding of quantified hypotheses for induction/destruction
when used in Ltac.
 Fixing bad parentheses check in "pose (f binders := ...)" syntax.
 Fixing unbalanced parenthesis in Ltac debug trace printer.
 Fixing missing sort unification check in lemma application (bug #2084).
 Fixing "as" clause of "apply in" that was not working in the general case.
 Fixing eauto not using external hints with no pattern.
Tools and development
 Fixing missing c option in coq_makefile.
 Temporary hack for coqide.byte "double free or corruption" problem.
 Added support for code development under Bazaar.
 Added support for compilation under Solaris (thanks to Eric Le Lay, #2078).
 Parsing fixes and support for parsing regular comments inline in coqdoc,
using option parsecomments (suggestions by B. Pierce).
Changes from V8.1 to V8.2
=========================
Language
 If a fixpoint is not written with an explicit { struct ... }, then
all arguments are tried successively (from left to right) until one is
found that satisfies the structural decreasing condition.
 New experimental typeclass system giving adhoc polymorphism and
overloading based on dependent records and implicit arguments.
 New syntax "let 'pat := b in c" for letbinding using irrefutable patterns.
 New syntax "forall {A}, T" for specifying maximally inserted implicit
arguments in terms.
 Sort of Record/Structure, Inductive and CoInductive defaults to Type
if omitted.
 Support for optional "where" notation clauses for record fields.
 (Co)Inductive types can be defined as records
(e.g. "CoInductive stream := { hd : nat; tl : stream }.")
 New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent
statements.
 Support for sortpolymorphism on constants denoting inductive types.
 Several evolutions of the module system (handling of module aliases,
functorial module types, an Include feature, etc).
 Prop now a subtype of Set (predicative and impredicative forms).
 Recursive inductive types in Prop with a single constructor of which
all arguments are in Prop is now considered to be a singleton
type. It consequently supports all eliminations to Prop, Set and Type.
As a consequence, Acc_rect has now a more direct proof [possible source
of easily fixed incompatibility in case of manual definition of a recursor
in a recursive singleton inductive type].
 New syntax to do implicit generalization in binders and inside terms.
 New tentative syntax for introduction of record objects without mentioning
the constructor { field := body; ... }, turning missing fields into holes
(compatible with refine and Program).
Vernacular commands
 Added option Global to "Arguments Scope" for section surviving.
 Added option "Unset Elimination Schemes" to deactivate the automatic
generation of elimination schemes.
 Modification of the Scheme command so you can ask for the name to be
automatically computed (e.g. Scheme Induction for nat Sort Set).
 New command "Combined Scheme" to build combined mutual induction
principles from existing mutual induction principles.
 New command "Scheme Equality" to build a decidable (boolean) equality
for simple inductive datatypes and a decision property over this equality
(e.g. Scheme Equality for nat).
 Added option "Set Equality Scheme" to make automatic the declaration
of the boolean equality when possible.
 Source of universe inconsistencies now printed when option
"Set Printing Universes" is activated.
 New option "Set Printing Existential Instances" for making the display of
existential variable instances explicit.
 Support for option "[id1 ... idn]", and "[id1 ... idn]", for the
"compute"/"cbv" reduction strategy, respectively meaning reduce only, or
everything but, the constants id1 ... idn. "lazy" alone or followed by
"[id1 ... idn]", and "[id1 ... idn]" also supported, meaning apply
all of betaiotazetadelta, possibly restricting delta.
 New command "Strategy" to control the expansion of constants during
conversion tests. It generalizes commands Opaque and Transparent by
introducing a range of levels. Lower levels are assigned to constants
that should be expanded first.
 New options Global and Local to Opaque and Transparent.
 New command "Print Assumptions" to display all variables, parameters
or axioms a theorem or definition relies on.
 "Add Rec LoadPath" now provides references to libraries using partially
qualified names (this holds also for coqtop/coqc option R).
 SearchAbout supports negated search criteria, reference to logical objects
by their notation, and more generally search of subterms.
 "Declare ML Module" now allows to import .cmxs files when Coq is
compiled in native code with a version of OCaml that supports native
Dynlink (>= 3.11).
 New command "Create HintDb name [discriminated]" to explicitely declare
a new hint database and optionaly turn on a discrimination net
implementation to index all the lemmas in the database.
 New commands "Hint Transparent" and "Hint Opaque" to set the unfolding
status of definitions used by auto. This information is taken into account
by the discrimination net and the unification algorithm.
 "Hint Extern" now takes an optional pattern and applies the given tactic
all the time if no pattern is given.
 Specific sort constraints on Record now taken into account.
 "Print LoadPath" supports a path argument to filter the display.
Libraries
 Several parts of the libraries are now in Type, in particular FSets,
SetoidList, ListSet, Sorting, Zmisc. This may induce a few
incompatibilities. In case of trouble while fixing existing development,
it may help to simply declare Set as an alias for Type (see file
SetIsType).
 New arithmetical library in theories/Numbers. It contains:
* an abstract modular development of natural and integer arithmetics
in Numbers/Natural/Abstract and Numbers/Integer/Abstract
* an implementation of efficient computational bounded and unbounded
integers that can be mapped to processor native arithmetics.
See Numbers/Cyclic/Int31 for 31bit integers and Numbers/Natural/BigN
for unbounded natural numbers and Numbers/Integer/BigZ for unbounded
integers.
* some proofs that both older libraries Arith, ZArith and NArith and
newer BigN and BigZ implement the abstract modular development.
This allows in particular BigN and BigZ to already come with a
large database of basic lemmas and some generic tactics (ring),
This library has still an experimental status, as well as the
processoracceleration mechanism, but both its abstract and its
concrete parts are already quite usable and could challenge the use
of nat, N and Z in actual developments. Moreover, an extension of
this framework to rational numbers is ongoing, and an efficient
Q structure is already provided (see Numbers/Rational/BigQ), but
this part is currently incomplete (no abstract layer and generic
lemmas).
 Many changes in FSets/FMaps. In practice, compatibility with earlier
version should be fairly good, but some adaptations may be required.
* Interfaces of unordered ("weak") and ordered sets have been factorized
thanks to new features of Coq modules (in particular Include), see
FSetInterface. Same for maps. Hints in these interfaces have been
reworked (they are now placed in a "set" database).
* To allow full subtyping between weak and ordered sets, a field
"eq_dec" has been added to OrderedType. The old version of OrderedType
is now called MiniOrderedType and functor MOT_to_OT allow to
convert to the new version. The interfaces and implementations
of sets now contain also such a "eq_dec" field.
* FSetDecide, contributed by Aaron Bohannon, contains a decision
procedure allowing to solve basic setrelated goals (for instance,
is a point in a particular set ?). See FSetProperties for examples.
* Functors of properties have been improved, especially the ones about
maps, that now propose some induction principles. Some properties
of fold need less hypothesis.
* More uniformity in implementations of sets and maps: they all use
implicit arguments, and no longer export unnecessary scopes (see
bug #1347)
* Internal parts of the implementations based on AVL have evolved a
lot. The main files FSetAVL and FMapAVL are now much more
lightweight now. In particular, minor changes in some functions
has allowed to fully separate the proofs of operational
correctness from the proofs of wellbalancing: wellbalancing is
critical for efficiency, but not anymore for proving that these
trees implement our interfaces, hence we have moved these proofs
into appendix files FSetFullAVL and FMapFullAVL. Moreover, a few
functions like union and compare have been modified in order to be
structural yet efficient. The appendix files also contains
alternative versions of these few functions, much closer to the
initial Ocaml code and written via the Function framework.
 Library IntMap, subsumed by FSets/FMaps, has been removed from
Coq Standard Library and moved into a user contribution Cachan/IntMap
 Better computational behavior of some constants (eq_nat_dec and
le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare
transparent, ...) (exceptional source of incompatibilities).
 Boolean operators moved from module Bool to module Datatypes (may need
to rename qualified references in script and force notations  and &&
to be at levels 50 and 40 respectively).
 The constructors xI and xO of type positive now have postfix notations
"~1" and "~0", allowing to write numbers in binary form easily, for instance
6 is 1~1~0 and 4*p is p~0~0 (see BinPos.v).
 Improvements to NArith (Nminus, Nmin, Nmax), and to QArith (in particular
a better power function).
 Changes in ZArith: several additional lemmas (used in theories/Numbers),
especially in Zdiv, Znumtheory, Zpower. Moreover, many results in
Zdiv have been generalized: the divisor may simply be nonnull
instead of strictly positive (see lemmas with name ending by
"_full"). An alternative file ZOdiv proposes a different behavior
(the one of Ocaml) when dividing by negative numbers.
 Changes in Arith: EqNat and Wf_nat now exported from Arith, some
constructions on nat that were outside Arith are now in (e.g. iter_nat).
 In SetoidList, eqlistA now expresses that two lists have similar elements
at the same position, while the predicate previously called eqlistA
is now equivlistA (this one only states that the lists contain the same
elements, nothing more).
 Changes in Reals:
* Most statement in "sigT" (including the
completeness axiom) are now in "sig" (in case of incompatibility,
use proj1_sig instead of projT1, sig instead of sigT, etc).
* More uniform naming scheme (identifiers in French moved to English,
consistent use of 0  zero  instead of O  letter O , etc).
* Lemma on prod_f_SO is now on prod_f_R0.
* Useless hypothesis of ln_exists1 dropped.
* New Rlogic.v states a few logical properties about R axioms.
* RIneq.v extended and made cleaner.
 Slight restructuration of the Logic library regarding choice and classical
logic. Addition of files providing intuitionistic axiomatizations of
descriptions: Epsilon.v, Description.v and IndefiniteDescription.v.
 Definition of pred and minus made compatible with the structural
decreasing criterion for use in fixpoints.
 Files Relations/Rstar.v and Relations/Newman.v moved out to the user
contribution repository (contribution CoC_History). New lemmas about
transitive closure added and some bound variables renamed (exceptional
risk of incompatibilities).
Notations, coercions, implicit arguments and type inference
 More automation in the inference of the return clause of dependent
patternmatching problems.
 Experimental allowance for omission of the clauses easily detectable as
impossible in patternmatching problems.
 Improved inference of implicit arguments, now working inside record
declarations.
 New options "Set Maximal Implicit Insertion", "Set Reversible Pattern
Implicit", "Set Strongly Strict Implicit" and "Set Printing Implicit
Defensive" for controlling inference and use of implicit arguments.
 New modifier in "Implicit Arguments" to force an implicit argument to
be maximally inserted.
 New options Global and Local to "Implicit Arguments" for section
surviving or non export outside module.
 Level "constr" moved from 9 to 8.
 Structure/Record now printed as Record (unless option Printing All is set).
 Support for parametric notations defining constants.
 Insertion of coercions below product types refrains to unfold
constants (possible source of incompatibility).
 New support for fix/cofix in notations.
Tactic Language
 Secondorder patternmatching now working in Ltac "match" clauses
(syntax for secondorder unification variable is "@?X").
 Support for matching on let bindings in match context using syntax
"H := body" or "H := body : type".
 (?X ?Y) patterns now match any application instead of only unary
applications (possible source of incompatibility).
 Ltac accepts integer arguments (syntax is "ltac:nnn" for nnn an integer).
 The general sequence tactical "expr_0 ; [ expr_1  ...  expr_n ]"
is extended so that at most one expr_i may have the form "expr .."
or just "..". Also, n can be different from the number of subgoals
generated by expr_0. In this case, the value of expr (or idtac in
case of just "..") is applied to the intermediate subgoals to make
the number of tactics equal to the number of subgoals.
 A name used as the name of the parameter of a lemma (like f in
"apply f_equal with (f:=t)") is now interpreted as a ltac variable
if such a variable exists (this is a possible source of
incompatibility and it can be fixed by renaming the variables of a
ltac function into names that do not clash with the lemmas
parameter names used in the tactic).
 New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression.
 "let rec ... in ... " now supported for expressions without explicit
parameters; interpretation is lazy to the contrary of "let ... in ...";
hence, the "rec" keyword can be used to turn the argument of a
"let ... in ..." into a lazy one.
 Patterns for hypotheses types in "match goal" are now interpreted in
type_scope.
 A bound variable whose name is not used elsewhere now serves as
metavariable in "match" and it gets instantiated by an identifier
(allow e.g. to extract the name of a statement like "exists x, P x").
 New printing of Ltac call trace for better debugging.
 The Czar (formerly know as declarative) proof language is now properly
documented.
Tactics
 New tactics "apply > term", "apply < term", "apply > term in
ident", "apply < term in ident" for applying equivalences (iff).
 "apply" and "rewrite" now take open terms (terms with undefined existentials)
as input.
 Slight improvement of the hnf and simpl tactics when applied on
expressions with explicit occurrences of match or fix.
 New tactics "eapply in", "erewrite", "erewrite in".
 New tactics "ediscriminate", "einjection", "esimplify_eq".
 Tactics "discriminate", "injection", "simplify_eq" now support any
term as argument. Clause "with" is also supported.
 Unfoldable references can be given by notation's string rather than by name
in unfold.
 The "with" arguments are now typed using informations from the current goal:
allows support for coercions and more inference of implicit arguments.
 Application of "f_equal"style lemmas works better.
 Tactics elim, case, destruct and induction now support variants eelim,
ecase, edestruct and einduction.
 Tactics destruct and induction now support the "with" option and the
"in" clause option. If the option "in" is used, an equality is added
to remember the term to which the induction or case analysis applied
(possible source of parsing incompatibilities when destruct or induction is
part of a letin expression in Ltac; extra parentheses are then required).
 New support for "as" clause in tactics "apply in" and "eapply in".
 Some new intro patterns:
* intro pattern "?A" genererates a fresh name based on A.
Caveat about a slight loss of compatibility:
Some intro patterns don't need space between them. In particular
intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it
is still legal but equivalent to intros ?a ?b.
* intro pattern "(A & ... & Y & Z)" synonym to "(A,....,(Y,Z)))))"
for rightassociative constructs like /\ or exists.
 Several syntax extensions concerning "rewrite":
* "rewrite A,B,C" can be used to rewrite A, then B, then C. These rewrites
occur only on the first subgoal: in particular, sideconditions of the
"rewrite A" are not concerned by the "rewrite B,C".
* "rewrite A by tac" allows to apply tac on all sideconditions generated by
the "rewrite A".
* "rewrite A at n" allows to select occurrences to rewrite: rewrite only
happen at the nth exact occurrence of the first successful matching of
A in the goal.
* "rewrite 3 A" or "rewrite 3!A" is equivalent to "rewrite A,A,A".
* "rewrite !A" means rewriting A as long as possible (and at least once).
* "rewrite 3?A" means rewriting A at most three times.
* "rewrite ?A" means rewriting A as long as possible (possibly never).
* many of the above extensions can be combined with each other.
 Introduction patterns better respect the structure of context in presence of
missing or extra names in nested disjunctionconjunction patterns [possible
source of rare incompatibilities].
 New syntax "rename a into b, c into d" for "rename a into b; rename c into d"
 New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]"
to do inductioninversion on instantiated inductive families � la BasicElim.
 Tactics "apply" and "apply in" now able to reason modulo unfolding of
constants (possible source of incompatibility in situations where apply
may fail, e.g. as argument of a try or a repeat and in a ltac function);
versions that do not unfold are renamed into "simple apply" and
"simple apply in" (usable for compatibility or for automation).
 Tactics "apply" and "apply in" now able to traverse conjunctions and to
select the first matching lemma among the components of the conjunction;
tactic "apply" also able to apply lemmas of conclusion an empty type.
 Tactic "apply" now supports application of several lemmas in a row.
 Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)".
 New tactic "instantiate" (without argument).
 Tactic firstorder "with" and "using" options have their meaning swapped for
consistency with auto/eauto (source of incompatibility).
 Tactic "generalize" now supports "at" options to specify occurrences
and "as" options to name the quantified hypotheses.
 New tactic "specialize H with a" or "specialize (H a)" allows to transform
inplace a universallyquantified hypothesis (H : forall x, T x) into its
instantiated form (H : T a). Nota: "specialize" was in fact there in earlier
versions of Coq, but was undocumented, and had a slightly different behavior.
 New tactic "contradict H" can be used to solve any kind of goal as long as
the user can provide afterwards a proof of the negation of the hypothesis H.
If H is already a negation, say ~T, then a proof of T is asked.
If the current goal is a negation, say ~U, then U is saved in H afterwards,
hence this new tactic "contradict" extends earlier tactic "swap", which is
now obsolete.
 Tactics f_equal is now done in ML instead of Ltac: it now works on any
equality of functions, regardless of the arity of the function.
 New options "before id", "at top", "at bottom" for tactics "move"/"intro".
 Some more debug of reflexive omega (romega), and internal clarifications.
Moreover, romega now has a variant "romega with *" that can be also used
on nonZ goals (nat, N, positive) via a call to a translation tactic named
zify (its purpose is to Zify your goal...). This zify may also be used
independantly of romega.
 Tactic "remember" now supports an "in" clause to remember only selected
occurrences of a term.
 Tactic "pose proof" supports name overwriting in case of specialization of an
hypothesis.
 Semidecision tactic "jp" for firstorder intuitionistic logic moved to user
contributions (subsumed by "firstorder").
Program
 Moved useful tactics in theories/Program and documented them.
 Add Program.Basics which contains standard definitions for functional
programming (id, apply, flip...)
 More robust obligation handling, dependent patternmatching and
wellfounded definitions.
 Program CoFixpoint is accepted, Program Fixpoint uses the new way to infer
which argument decreases structurally.
 Program Lemma, Axiom etc... now permit to have obligations in the statement
iff they can be automatically solved by the default tactic.
 Renamed "Obligations Tactic" command to "Obligation Tactic".
 New command "Preterm [ of id ]" to see the actual term fed to Coq for
debugging purposes.
 New option "Transparent Obligations" to control the declaration of
obligations as transparent or opaque. All obligations are now transparent
by default, otherwise the system declares them opaque if possible.
 Changed the notations "left" and "right" to "in_left" and "in_right" to hide
the proofs in standard disjunctions, to avoid breaking existing scripts when
importing Program. Also, put them in program_scope.
Type Classes
 New "Class", "Instance" and "Program Instance" commands to define
classes and instances documented in the reference manual.
 New binding construct "`{Class_1 param_1 .. param_n, Class_2 ...}"
for binding type classes, usable everywhere.
 New command " Print Classes " and " Print Instances some_class " to
print tables for typeclasses.
 New default eauto hint database "typeclass_instances" used by the default
typeclass instance search tactic.
 New theories directory "theories/Classes" for standard typeclasses
declarations. Module Classes.RelationClasses is a typeclass port of
Relation_Definitions plus a generic development of algebra on
nary heterogeneous predicates.
Setoid rewriting
 Complete (and still experimental) rewrite of the tactic
based on typeclasses. The old interface and semantics are
almost entirely respected, except:
 Import Setoid is now mandatory to be able to call setoid_replace
and declare morphisms.
 ">", "++>" and "==>" are now right associative notations
declared at level 55 in scope signature_scope.
Their introduction may break existing scripts that defined
them as notations with different levels.
 One can use [Typeclasses Opaque/Transparent [cst]] to indicate
that [cst] should not be unfolded during unification for morphism
resolution, by default all constants are transparent.
 The [setoid_rewrite]'s semantics change when rewriting with
a lemma: it can rewrite two different instantiations of the lemma
at once. Use [setoid_rewrite H at 1] for (almost) the usual semantics.
[setoid_rewrite] will also try to rewrite under binders now, and can
succeed on different terms than before. In particular, it will unify under
letbound variables. When called through [rewrite], the semantics are
unchanged though.
 [Add Morphism term : id] has different semantics when used with
parametric morphism: it will try to find a relation on the parameters
too. The behavior has also changed with respect to default relations:
the most recently declared Setoid/Relation will be used, the documentation
explains how to customize this behavior.
 Parametric Relation and Morphism are declared differently, using the
new [Add Parametric] commands, documented in the manual.
 Setoid_Theory is now an alias to Equivalence, scripts building objects
of type Setoid_Theory need to unfold (or [red]) the definitions
of Reflexive, Symmetric and Transitive in order to get the same goals
as before. Scripts which introduced variables explicitely will not break.
 The order of subgoals when doing [setoid_rewrite] with sideconditions
is now always the same: first the new goal, then the conditions.
 New standard library modules Classes.Morphisms declares
standard morphisms on refl/sym/trans relations.
Classes.Morphisms_Prop declares morphisms on propositional
connectives and Classes.Morphisms_Relations on generalized predicate
connectives. Classes.Equivalence declares notations and tactics
related to equivalences and Classes.SetoidTactics defines the
setoid_replace tactics and some support for the "Add *" interface,
notably the tactic applied automatically before each "Add Morphism"
proof.
 Userdefined subrelations are supported, as well as higherorder morphisms
and rewriting under binders. The tactic is also extensible entirely in Ltac.
The documentation has been updated to cover these features.
 [setoid_rewrite] and [rewrite] now support the [at] modifier to select
occurrences to rewrite, and both use the [setoid_rewrite] code, even when
rewriting with leibniz equality if occurrences are specified.
Extraction
 Improved behavior of the Caml extraction of modules: name clashes should
not happen anymore.
 The command Extract Inductive has now a syntax for infix notations. This
allows in particular to map Coq lists and pairs onto Caml ones:
Extract Inductive list => list [ "[]" "(::)" ].
Extract Inductive prod => "(*)" [ "(,)" ].
 In pattern matchings, a default pattern " _ > ..." is now used whenever
possible if several branches are identical. For instance, functions
corresponding to decidability of equalities are now linear instead of
quadratic.
 A new instruction Extraction Blacklist id1 .. idn allows to prevent filename
conflits with existing code, for instance when extracting module List
to Ocaml.
CoqIDE
 CoqIDE font defaults to monospace so as indentation to be meaningful.
 CoqIDE supports nested goals and any other kind of declaration in the middle
of a proof.
 Undoing nontactic commands in CoqIDE works faster.
 New CoqIDE menu for activating display of various implicit informations.
 Added the possibility to choose the location of tabs in coqide:
(in Edit>Preferences>Misc)
 New Open and Save As dialogs in CoqIDE which filter *.v files.
Tools
 New standalone .vo files verifier "coqchk".
 Extended I coqtop/coqc option to specify a logical dir: "I dir as coqdir".
 New coqtop/coqc option excludedir to exclude subdirs for option R.
 The binary "parser" has been renamed to "coqparser".
coqdoc
 Improved coqdoc and dump of globalization information to give more
metainformation on identifiers. All categories of Coq definitions are
supported, which makes typesetting trivial in the generated documentation.
 A "interpolate" option permits to use typesetting information from the
typechecked part of the file to typeset identifiers appearing in Coq escapings
inside the documentation.
 Better handling of utf8 ("utf8" option) and respect of spaces in the source.
 Support for hyperlinking and indexing developments in the TeX output.
 New option "color" of the coqdoc style file to render identifiers using colors.
 Additional macros in the TeX ouput allowing to customize indentation and size of
empty lines. New environment "coqdoccode" for Coq code.
Miscellaneous
 Coq installation provides enough files so that Ocaml's extensions need not
the Coq sources to be compiled (this assumes O'Caml 3.10 and Camlp5).
 New commands "Set Whelp Server" and "Set Whelp Getter" to customize the
Whelp search tool.
 Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into
"Test Printing Let for ref" and "Test Printing If for ref".
 An overhauled build system (new Makefiles); see dev/doc/buildsystem.txt.
 Add browser option to configure script.
 Build a shared library for the C part of Coq, and use it by default on
non(Windows or MacOS) systems. Bytecode executables are now pure. The
behaviour is configurable with coqrunbyteflags, coqtoolsbyteflags and
custom configure options.
 Complexity tests can be skipped by setting the environment variable
COQTEST_SKIPCOMPLEXITY.
Changes from V8.1gamma to V8.1
==============================
Bug fixes
 Many bugs have been fixed (cf coqbugs web page)
Tactics
 New tactics ring, ring_simplify and new tactic field now able to manage
power to a positive integer constant. Tactic ring on Z and R, and
field on R manage power (may lead to incompatibilities with V8.1gamma).
 Tactic field_simplify now applicable in hypotheses.
 New field_simplify_eq for simplifying field equations into ring equations.
 Tactics ring, ring_simplify, field, field_simplify and field_simplify_eq
all able to apply usergiven equations to rewrite monoms on the fly
(see documentation).
Libraries
 New file ConstructiveEpsilon.v defining an epsilon operator and
proving the axiom of choice constructively for a countable domain
and a decidable predicate.
Changes from V8.1beta to V8.1gamma
==================================
Syntax
 changed parsing precedence of let/in and fun constructions of Ltac:
let x := t in e1; e2 is now parsed as let x := t in (e1;e2).
Language and commands
 Added sortpolymorphism for definitions in Type (but finally abandonned).
 Support for implicit arguments in the types of parameters in
(co)fixpoints and (co)inductive declarations.
 Improved type inference: use as much of possible general information.
before applying irreversible unification heuristics (allow e.g. to
infer the predicate in "(exist _ 0 (refl_equal 0) : {n:nat  n=0 })").
 Support for MillerPfenning's patterns unification in type synthesis
(e.g. can infer P such that P x y = phi(x,y)).
 Support for "where" clause in cofixpoint definitions.
 New option "Set Printing Universes" for making Type levels explicit.
Tactics
 Improved implementation of the ring and field tactics. For compatibility
reasons, the previous tactics are renamed as legacy ring and legacy field,
but should be considered as deprecated.
 New declarative mathematical proof language.
 Support for argument lists of arbitrary length in Tactic Notation.
 [rewrite ... in H] now fails if [H] is used either in an hypothesis
or in the goal.
 The semantics of [rewrite ... in *] has been slightly modified (see doc).
 Support for "as" clause in tactic injection.
 New forwardreasoning tactic "apply in".
 Ltac fresh operator now builds names from a concatenation of its arguments.
 New ltac tactic "remember" to abstract over a subterm and keep an equality
 Support for MillerPfenning's patterns unification in apply/rewrite/...
(may lead to few incompatibilities  generally now useless tactic calls).
Bug fixes
 Fix for notations involving basic "match" expressions.
 Numerous other bugs solved (a few fixes may lead to incompatibilities).
Changes from V8.0 to V8.1beta
=============================
Logic
 Added sortpolymorphism on inductive families
 Allowance for recursively non uniform parameters in inductive types
Syntax
 No more support for version 7 syntax and for translation to version 8 syntax.
 In fixpoints, the { struct ... } annotation is not mandatory any more when
only one of the arguments has an inductive type
 Added disjunctive patterns in matchwith patterns
 Support for primitive interpretation of string literals
 Extended support for Unicode ranges
Vernacular commands
 Added "Print Ltac qualid" to print a user defined tactic.
 Added "Print Rewrite HintDb" to print the content of a DB used by
autorewrite.
 Added "Print Canonical Projections".
 Added "Example" as synonym of "Definition".
 Added "Proposition" and "Corollary" as extra synonyms of "Lemma".
 New command "Whelp" to send requests to the Helm database of proofs
formalized in the Calculus of Inductive Constructions.
 Command "functional induction" has been reimplemented from the new
"Function" command.
Ltac and tactic syntactic extensions
 New primitive "external" for communication with tool external to Coq
 New semantics for "match t with": 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" does). The keyword "lazymatch" can be used to delay the
evaluation of tactics occurring in matching clauses.
 Hint base names can be parametric in auto and trivial.
 Occurrence values can be parametric in unfold, pattern, etc.
 Added entry constr_may_eval for tactic extensions.
 Lowpriority term printer made available in MLwritten tactic extensions.
 "Tactic Notation" extended to allow notations of tacticals.
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).
 New implementation (still experimental) of the ring tactic with a builtin
notion of coefficients and a better usage of setoids.
 New conversion tactic "vm_compute": evaluates the goal (or an hypothesis)
with a callbyvalue strategy, using the compiled version of terms.
 When rewriting H where H is not directly a Coq equality, search first H for
a registered setoid equality before starting to reduce in H. This is unlikely
to break any script. Should this happen nonetheless, one can insert manually
some "unfold ... in H" before rewriting.
 Fixed various bugs about (setoid) rewrite ... in ... (in particular #1101)
 "rewrite ... in" now accepts a clause as place where to rewrite instead of
juste a simple hypothesis name. For instance:
rewrite H in H1,H2  * means rewrite H in H1; rewrite H in H2; rewrite H
rewrite H in *  will do try rewrite H in Hi for all hypothesis Hi <> H.
 Added "dependent rewrite term" and "dependent rewrite term in hyp".
 Added "autorewrite with ... in hyp [using ...]".
 Tactic "replace" now accepts a "by" tactic clause.
 Added "clear  id" to clear all hypotheses except the ones depending in id.
 The argument of Declare Left Step and Declare Right Step is now a term
(it used to be a reference).
 Omega now handles arbitrary precision integers.
 Several bug fixes in Reflexive Omega (romega).
 Idtac can now be left implicit in a [......] construct: for instance,
[ foo   bar ] stands for [ foo  idtac  bar ].
 Fixed a "fold" bug (non critical but 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.
 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.
 Introduction patterns now support side hypotheses (e.g. intros [] on
"(nat > nat) > nat" works).
 New introduction patterns ">" and "<" for immediate rewriting of
introduced hypotheses.
 Introduction patterns coming after non trivial introduction patterns now
force full introduction of the first pattern (e.g. "intros [[] p]" on
"nat>nat>nat" now behaves like "intros [[?] p]")
 Added "eassumption".
 Added option 'using lemmas' to auto, trivial and eauto.
 Tactic "congruence" is now complete for its intended scope (ground
equalities and inequalities with constructors). Furthermore, it
tries to equates goal and hypotheses.
 New tactic "rtauto" solves pure propositional logic and gives a
reflective version of the available proof.
 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 "matchwith" construct (use "Set Printing All"
to see hidden occurrences).
 Generalization of induction "induction x1...xn using scheme" where
scheme is an induction principle with complex predicates (like the
ones generated by function induction).
 Some small Ltac tactics has been added to the standard library
(file Tactics.v):
* f_equal : instead of using the different f_equalX lemmas
* case_eq : a "case" without loss of information. An equality
stating the current situation is generated in every subcases.
* swap : for a negated goal ~B and a negated hypothesis H:~A,
swap H asks you to prove A from hypothesis B
* revert : revert H is generalize H; clear H.
Extraction
 All type parts should now disappear instead of sometimes producing _
(for instance in Map.empty).
 Haskell extraction: types of functions are now printed, better
unsafeCoerce mechanism, both for hugs and ghc.
 Scheme extraction improved, see http://www.pps.jussieu.fr/~letouzey/scheme.
 Many bug fixes.
Modules
 Added "Locate Module qualid" to get the full path of a module.
 Module/Declare Module syntax made more uniform.
 Added syntactic sugar "Declare Module Export/Import" and
"Module Export/Import".
 Added syntactic sugar "Module M(Export/Import X Y: T)" and
"Module Type M(Export/Import X Y: T)"
(only for interactive definitions)
 Construct "with" generalized to module paths:
T with (DefinitionModule) M1.M2....Mn.l := l'.
Notations
 Option "format" aware of recursive notations.
 Added insertion of spaces by default in recursive notations w/o separators.
 No more automatic printing box in case of userprovided printing "format".
 New notation "exists! x:A, P" for unique existence.
 Notations for specific numerals now compatible with generic notations of
numerals (e.g. "1" can be used to denote the unit of a group without
hiding 1%nat)
Libraries
 New library on String and Ascii characters (contributed by L. Thery).
 New library FSets+FMaps of finite sets and maps.
 New library QArith on rational numbers.
 Small extension of Zmin.V, new Zmax.v, new Zminmax.v.
 Reworking and extension of the files on classical logic and
description principles (possible incompatibilities)
 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).
 Restructuration of Eqdep_dec.v and Eqdep.v: more lemmas in Type.
 Znumtheory now contains a gcd function that can compute within Coq.
 More lemmas stated on Type in Wf.v, removal of redundant Acc_iter and
Acc_iter2.
 Change of the internal names of lemmas in OmegaLemmas.
 Acc in Wf.v and clos_refl_trans in Relation_Operators.v now rely on
the allowance for recursively non uniform parameters (possible
source of incompatibilities: explicit patternmatching on these
types may require to remove the occurrence associated to their
recursively non uniform parameter).
 Coq.List.In_dec has been set transparent (this may exceptionally break
proof scripts, set it locally opaque for compatibility).
 More on permutations of lists in List.v and Permutation.v.
 List.v has been much expanded.
 New file SetoidList.v now contains results about lists seen with
respect to a setoid equality.
 Library NArith has been expanded, mostly with results coming from
Intmap (for instance a bitwise xor), plus also a bridge between N and
Bitvector.
 Intmap has been reorganized. In particular its address type "addr" is
now N. User contributions known to use Intmap have been adapted
accordingly. If you're using this library please contact us.
A wrapper FMapIntMap now presents Intmap as a particular implementation
of FMaps. New developments are strongly encouraged to use either this
wrapper or any other implementations of FMap instead of using directly
this obsolete Intmap.
Tools
 New semantics for coqtop options ("batch" expects option "top dir"
for loading vernac file that contains definitions).
 Tool coq_makefile now removes custom targets that are file names in
"make clean"
 New environment variable 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.
Changes from V8.0beta to V8.0
=============================
Vernacular commands
 New option "Set Printing All" to deactivate all highlevel forms of
printing (implicit arguments, coercions, destructing let,
ifthenelse, 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 preV8 Grammar/Syntax commands
 Command "Print." discontinued.
 Redundant syntax "Implicit Arguments On/Off" discontinued
New syntax
 Semantics change of the ifthenelse 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 coqbugs 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 doublebackquotes 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
 isolatin1 characters are no longer supported: move your files to
7bits 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 etareduced predicates
Changes from V7.4 to V8.0beta old syntax
========================================
Logic
 Set now predicative by default
 New option impredicativeset 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.
 "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 dontloadproofs 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
 Many newly supported UTF8 encoded unicode blocks
 Greek letters (038003FF), Hebrew letters (U05D005EF), letterlike
symbols (2100214F, that includes double N,Z,Q,R), prime
signs (from 20802089) and characters from many written languages
are valid in identifiers
 mathematical operators (220022FF), supplemental mathematical
operators (2A002AFF), miscellaneous technical (230023FF that
includes sqrt symbol), miscellaneous symbols (260026FF), arrows
(219021FF and 2900297F), invisible mathematical operators (from
20802089), ... are valid 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 righthandside 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 noninductive 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 coqbugs 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
retypecheckability of the printed term
 In Grammar command, the only predefined nonterminal 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".
 Theoremlike 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 sideeffect, 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 userprovided elimination scheme
 NewDestruct and NewInduction now accept userprovided 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 collisionavoiding
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 typecheck,
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 prooftrees (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
MLside 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 letin fixed (#238)
 Inversion bugs fixed (#212 and #220)
 Omega bug related to Set fixed (#180)
 Typechecking inefficiency of nested destructuring letin fixed (#216)
 Improved handling of letin 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 nonrecursivity 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 patternmatching (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 letin's fixed
 Bug unexpected Delta with letin 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 dumpglob 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
letin 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 axiomfree.
 In [Sets], Integers.v now based on nat
 In [Arith], more lemmas in Min.v, new file Max.v, tailrecursive
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 letin and recursively dependent hypotheses fixed
 Syntax [x:=t:T]u now allowed as mentioned in documentation
 Bug with recursive inductive types involving letin fixed
 Known patternmatching bugs fixed
 Known Cases elimination predicate bugs fixed
 Improved errors messages for patternmatching and projections
 Better error messages for illtyped 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 letin construct (see sections 1.2.8 and )
 Long names (see sections 2.6 and 2.7)
 New highlevel 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 "letin" construction

 New construction for local definitions (letin) 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 userfriendly
 New tactic NewDestruct and NewInduction intended to replace Elim
and Induction, Case and Destruct in a more userfriendly 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 "letin" (+)
 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``) (+)
 Prettyprinting 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 prettyprinting 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, SophiaAntipolis)
 Basic notions of graph theory [GRAPHSBASICS] (Jean Duprat, Lyon)
 A library for floatingpoint numbers [Float] (Laurent Th�ry, Sylvie Boldo,
SophiaAntipolis)
 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)
 Pautomaton 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] (JeanChristophe Filli�tre, Orsay)
 Correctness proofs of Buchberger's algorithm [Buchberger] and RSA
cryptographic algorithm [Rsa] (Laurent Th�ry, SophiaAntipolis)
 Correctness proof of Stalmarck tautology checker algorithm
[Stalmarck] (Laurent Th�ry, Pierre Letouzey, SophiaAntipolis)
