Early history of Coq — Coq 8.20+alpha documentation (2024)

\[\begin{split}\newcommand{\as}{\kw{as}}\newcommand{\case}{\kw{case}}\newcommand{\cons}{\textsf{cons}}\newcommand{\consf}{\textsf{consf}}\newcommand{\emptyf}{\textsf{emptyf}}\newcommand{\End}{\kw{End}}\newcommand{\kwend}{\kw{end}}\newcommand{\even}{\textsf{even}}\newcommand{\evenO}{\textsf{even}_\textsf{O}}\newcommand{\evenS}{\textsf{even}_\textsf{S}}\newcommand{\Fix}{\kw{Fix}}\newcommand{\fix}{\kw{fix}}\newcommand{\for}{\textsf{for}}\newcommand{\forest}{\textsf{forest}}\newcommand{\Functor}{\kw{Functor}}\newcommand{\In}{\kw{in}}\newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)}\newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)}\newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}}\newcommand{\injective}{\kw{injective}}\newcommand{\kw}[1]{\textsf{#1}}\newcommand{\length}{\textsf{length}}\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}\newcommand{\List}{\textsf{list}}\newcommand{\lra}{\longrightarrow}\newcommand{\Match}{\kw{match}}\newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})}\newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})}\newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})}\newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})}\newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})}\newcommand{\mto}{.\;}\newcommand{\nat}{\textsf{nat}}\newcommand{\Nil}{\textsf{nil}}\newcommand{\nilhl}{\textsf{nil\_hl}}\newcommand{\nO}{\textsf{O}}\newcommand{\node}{\textsf{node}}\newcommand{\nS}{\textsf{S}}\newcommand{\odd}{\textsf{odd}}\newcommand{\oddS}{\textsf{odd}_\textsf{S}}\newcommand{\ovl}[1]{\overline{#1}}\newcommand{\Pair}{\textsf{pair}}\newcommand{\plus}{\mathsf{plus}}\newcommand{\SProp}{\textsf{SProp}}\newcommand{\Prop}{\textsf{Prop}}\newcommand{\return}{\kw{return}}\newcommand{\Set}{\textsf{Set}}\newcommand{\Sort}{\mathcal{S}}\newcommand{\Str}{\textsf{Stream}}\newcommand{\Struct}{\kw{Struct}}\newcommand{\subst}[3]{#1\{#2/#3\}}\newcommand{\tl}{\textsf{tl}}\newcommand{\tree}{\textsf{tree}}\newcommand{\trii}{\triangleright_\iota}\newcommand{\Type}{\textsf{Type}}\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}}\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}}\newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]}\newcommand{\WFE}[1]{\WF{E}{#1}}\newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)}\newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}\newcommand{\with}{\kw{with}}\newcommand{\WS}[3]{#1[] \vdash #2 <: #3}\newcommand{\WSE}[2]{\WS{E}{#1}{#2}}\newcommand{\WT}[4]{#1[#2] \vdash #3 : #4}\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}}\newcommand{\zeroone}[1]{[{#1}]}\end{split}\]

Historical roots¶

Coq is a proof assistant for higher-order logic, allowing thedevelopment of computer programs consistent with their formalspecification. It is the result of about ten years 1 of researchof the Coq project. We shall briefly survey here three main aspects: thelogical language in which we write our axiomatizations andspecifications, the proof assistant which allows the development ofverified mathematical proofs, and the program extractor whichsynthesizes computer programs obeying their formal specifications,written as logical assertions in the language.

The logical language used by Coq is a variety of type theory, called theCalculus of Inductive Constructions. Without going back to Leibniz andBoole, we can date the creation of what is now called mathematical logicto the work of Frege and Peano at the turn of the century. The discoveryof antinomies in the free use of predicates or comprehension principlesprompted Russell to restrict predicate calculus with a stratification oftypes. This effort culminated with Principia Mathematica, the firstsystematic attempt at a formal foundation of mathematics. Asimplification of this system along the lines of simply typedλ-calculus occurred with Church’s Simple Theory ofTypes. The λ-calculus notation, originally used forexpressing functionality, could also be used as an encoding of naturaldeduction proofs. This Curry-Howard isomorphism was used by N. de Bruijnin the Automath project, the first full-scale attempt to develop andmechanically verify mathematical proofs. This effort culminated withJutting’s verification of Landau’s Grundlagen in the 1970’s.Exploiting this Curry-Howard isomorphism, notable achievements in prooftheory saw the emergence of two type-theoretic frameworks; the firstone, Martin-Löf’s Intuitionistic Theory of Types, attempts a newfoundation of mathematics on constructive principles. The second one,Girard’s polymorphic λ-calculus $F_\omega$, is avery strong functional system in which we may represent higher-orderlogic proof structures. Combining both systems in a higher-orderextension of the Automath language, T. Coquand presented in 1985 thefirst version of the Calculus of Constructions, CoC. This stronglogical system allowed powerful axiomatizations, but direct inductivedefinitions were not possible, and inductive notions had to be definedindirectly through functional encodings, which introduced inefficienciesand awkwardness. The formalism was extended in 1989 by T. Coquand and C.Paulin with primitive inductive definitions, leading to the currentCalculus of Inductive Constructions. This extended formalism is notrigorously defined here. Rather, numerous concrete examples arediscussed. We refer the interested reader to relevant research papersfor more information about the formalism, its meta-theoretic properties,and semantics. However, it should not be necessary to understand thistheoretical material in order to write specifications. It is possible tounderstand the Calculus of Inductive Constructions at a higher level, asa mixture of predicate calculus, inductive predicate definitionspresented as typed PROLOG, and recursive function definitions close tothe language ML.

Automated theorem-proving was pioneered in the 1960’s by Davis andPutnam in propositional calculus. A complete mechanization (in the senseof a semidecision procedure) of classical first-order logic wasproposed in 1965 by J.A. Robinson, with a single uniform inference rulecalled resolution. Resolution relies on solving equations in freealgebras (i.e. term structures), using the unification algorithm. Manyrefinements of resolution were studied in the 1970’s, but few convincingimplementations were realized, except of course that PROLOG is in somesense issued from this effort. A less ambitious approach to proofdevelopment is computer-aided proof-checking. The most notableproof-checkers developed in the 1970’s were LCF, designed by R. Milnerand his colleagues at U. Edinburgh, specialized in proving propertiesabout denotational semantics recursion equations, and the Boyer andMoore theorem-prover, an automation of primitive recursion overinductive data types. While the Boyer-Moore theorem-prover attempted tosynthesize proofs by a combination of automated methods, LCF constructedits proofs through the programming of tactics, written in a high-levelfunctional meta-language, ML.

The salient feature which clearly distinguishes our proof assistant fromsay LCF or Boyer and Moore’s, is its possibility to extract programsfrom the constructive contents of proofs. This computationalinterpretation of proof objects, in the tradition of Bishop’sconstructive mathematics, is based on a realizability interpretation, inthe sense of Kleene, due to C. Paulin. The user must just mark hisintention by separating in the logical statements the assertions statingthe existence of a computational object from the logical assertionswhich specify its properties, but which may be considered as justcomments in the corresponding program. Given this information, thesystem automatically extracts a functional term from a consistency proofof its specifications. This functional term may be in turn compiled intoan actual computer program. This methodology of extracting programs fromproofs is a revolutionary paradigm for software engineering. Programsynthesis has long been a theme of research in artificial intelligence,pioneered by R. Waldinger. The Tablog system of Z. Manna and R.Waldinger allows the deductive synthesis of functional programs fromproofs in tableau form of their specifications, written in a variety offirst-order logic. Development of a systematic programming logic,based on extensions of Martin-Löf’s type theory, was undertaken atCornell U. by the Nuprl team, headed by R. Constable. The first actualprogram extractor, PX, was designed and implemented around 1985 by S.Hayashi from Kyoto University. It allows the extraction of a LISPprogram from a proof in a logical system inspired by the logicalformalisms of S. Feferman. Interest in this methodology is growing inthe theoretical computer science community. We can foresee the day whenactual computer systems used in applications will contain certifiedmodules, automatically generated from a consistency proof of theirformal specifications. We are however still far from being able to usethis methodology in a smooth interaction with the standard tools fromsoftware engineering, i.e. compilers, linkers, run-time systems takingadvantage of special hardware, debuggers, and the like. We hope that Coqcan be of use to researchers interested in experimenting with this newmethodology.

1: At the time of writing, i.e. 1995.

Versions 1 to 5¶

Note

This summary was written in 1995 together with the previoussection and formed the initial version of the Credits chapter.

A more comprehensive description of these early versions is availablein the following subsections, which come from a document written inSeptember 2015 by Gérard Huet, Thierry Coquand and Christine Paulin.

A first implementation of CoC was started in 1984 by G. Huet and T.Coquand. Its implementation language was CAML, a functional programminglanguage from the ML family designed at INRIA in Rocquencourt. The coreof this system was a proof-checker for CoC seen as a typedλ-calculus, called the Constructive Engine. This enginewas operated through a high-level notation permitting the declaration ofaxioms and parameters, the definition of mathematical types and objects,and the explicit construction of proof objects encoded asλ-terms. A section mechanism, designed and implemented byG. Dowek, allowed hierarchical developments of mathematical theories.This high-level language was called the Mathematical Vernacular.Furthermore, an interactive Theorem Prover permitted the incrementalconstruction of proof trees in a top-down manner, subgoaling recursivelyand backtracking from dead-ends. The theorem prover executed tacticswritten in CAML, in the LCF fashion. A basic set of tactics waspredefined, which the user could extend by his own specific tactics.This system (Version 4.10) was released in 1989. Then, the system wasextended to deal with the new calculus with inductive types by C.Paulin, with corresponding new tactics for proofs by induction. A newstandard set of tactics was streamlined, and the vernacular extended fortactics execution. A package to compile programs extracted from proofsto actual computer programs in CAML or some other functional languagewas designed and implemented by B. Werner. A new user-interface, relyingon a CAML-X interface by D. de Rauglaudre, was designed and implementedby A. Felty. It allowed operation of the theorem-prover through themanipulation of windows, menus, mouse-sensitive buttons, and otherwidgets. This system (Version 5.6) was released in 1991.

Coq was ported to the new implementation Caml-light of X. Leroy and D.Doligez by D. de Rauglaudre (Version 5.7) in 1992. A new version of Coqwas then coordinated by C. Murthy, with new tools designed by C. Parentto prove properties of ML programs (this methodology is dual to programextraction) and a new user-interaction loop. This system (Version 5.8)was released in May 1993. A Centaur interface CTCoq was then developedby Y. Bertot from the Croap project from INRIA-Sophia-Antipolis.

In parallel, G. Dowek and H. Herbelin developed a new proof engine,allowing the general manipulation of existential variables consistentlywith dependent types in an experimental version of Coq (V5.9).

The version V5.10 of Coq is based on a generic system for manipulatingterms with binding operators due to Chet Murthy. A new proof engineallows the parallel development of partial proofs for independentsubgoals. The structure of these proof trees is a mixed representationof derivation trees for the Calculus of Inductive Constructions withabstract syntax trees for the tactics scripts, allowing the navigationin a proof at various levels of details. The proof engine allows genericenvironment items managed in an object-oriented way. This newarchitecture, due to C. Murthy, supports several new facilities whichmake the system easier to extend and to scale up:

User-programmable tactics are allowed
It is possible to separately verify development modules, and to loadtheir compiled images without verifying them again - a quickrelocation process allows their fast loading
A generic parsing scheme allows user-definable notations, with asymmetric table-driven pretty-printer
Syntactic definitions allow convenient abbreviations
A limited facility of meta-variables allows the automatic synthesisof certain type expressions, allowing generic notations for e.g.equality, pairing, and existential quantification.

In the Fall of 1994, C. Paulin-Mohring replaced the structure ofinductively defined types and families by a new structure, allowing themutually recursive definitions. P. Manoury implemented a translation ofrecursive definitions into the primitive recursive style imposed by theinternal recursion operators, in the style of the ProPre system. C.Muñoz implemented a decision procedure for intuitionistic propositionallogic, based on results of R. Dyckhoff. J.C. Filliâtre implemented adecision procedure for first-order logic without contraction, based onresults of J. Ketonen and R. Weyhrauch. Finally C. Murthy implemented alibrary of inversion tactics, relieving the user from tediousdefinitions of “inversion predicates”.

Rocquencourt, Feb. 1st 1995

Gérard Huet

Version 1¶

This software is a prototype type checker for a higher-order logicalformalism known as the Theory of Constructions, presented in his PhDthesis by Thierry Coquand, with influences from Girard's system F andde Bruijn's Automath. The metamathematical analysis of the system isthe PhD work of Thierry Coquand. The software is mostly the work ofGérard Huet. Most of the mathematical examples verified with thesoftware are due to Thierry Coquand.

The programming language of the CONSTR software (as it was called atthe time) was a version of ML adapted from the Edinburgh LCF systemand running on a LISP backend. The main improvements from the originalLCF ML were that ML was compiled rather than interpreted (Gérard Huetbuilding on the original translator by Lockwood Morris), and that itwas enriched by recursively defined types (work of GuyCousineau). This ancestor of CAML was used and improved by LarryPaulson for his implementation of Cambridge LCF.

Software developments of this prototype occurred from late 1983 toearly 1985.

Version 1.10 was frozen on December 22nd 1984. It is the version usedfor the examples in Thierry Coquand's thesis, defended on January 31st1985. There was a unique binding operator, used both for universalquantification (dependent product) at the level of types andfunctional abstraction (λ) at the level of terms/proofs, in the mannerof Automath. Substitution (λ-reduction) was implemented using deBruijn's indexes.

Version 1.11 was frozen on February 19th, 1985. It is the version usedfor the examples in the paper: T. Coquand, G. Huet. Constructions: AHigher Order Proof System for Mechanizing Mathematics[CH85].

Christine Paulin joined the team at this point, for her DEA researchinternship. In her DEA memoir (August 1985) she presents developmentsfor the lambo function–$\text{lambo}(f)(n)$ computes the minimal$m$ such that $f(m)$ is greater than $n$, for $f$an increasing integer function, a challenge for constructive mathematics.She also encoded the majority voting algorithm of Boyer and Moore.

Version 2¶

The formal system, now renamed as the Calculus of Constructions, waspresented with a proof of consistency and comparisons with proofsystems of Per Martin Löf, Girard, and the Automath family of N. deBruijn, in the paper: T. Coquand and G. Huet. The Calculus ofConstructions[CH86b].

An abstraction of the software design, in the form of an abstractmachine for proof checking, and a fuller sequence of mathematicaldevelopments was presented in: T. Coquand, G. Huet. ConceptsMathématiques et Informatiques Formalisés dans le Calcul desConstructions[CH86a].

Version 2.8 was frozen on December 16th, 1985, and served fordeveloping the examples in the above papers.

This calculus was then enriched in version 2.9 with a cumulativehierarchy of universes. Universe levels were initially explicitnatural numbers. Another improvement was the possibility of automaticsynthesis of implicit type arguments, relieving the user of tediousredundant declarations.

Christine Paulin wrote an article Algorithm development in theCalculus of Constructions[Moh86]. Besides lambo and majority,she presents quicksort and a text formatting algorithm.

Version 2.13 of the Calculus of Constructions with universes wasfrozen on June 25th, 1986.

A synthetic presentation of type theory along constructive lines withML algorithms was given by Gérard Huet in his May 1986 CMU coursenotes Formal Structures for Computation and Deduction. Its chapterInduction and Recursion in the Theory of Constructions was presentedas an invited paper at the Joint Conference on Theory and Practice ofSoftware Development TAPSOFT’87 at Pise in March 1987, and publishedas Induction Principles Formalized in the Calculus ofConstructions[Hue88].

Version 3¶

This version saw the beginning of proof automation, with a searchalgorithm inspired from PROLOG and the applicative logic programmingprograms of the course notes Formal structures for computation anddeduction. The search algorithm was implemented in ML by ThierryCoquand. The proof system could thus be used in two modes: proofverification and proof synthesis, with tactics such as AUTO.

The implementation language was now called CAML, for CategoricalAbstract Machine Language. It used as backend the LLM3 virtual machineof Le Lisp by Jérôme Chailloux. The main developers of CAML wereMichel Mauny, Ascander Suarez and Pierre Weis.

V3.1 was started in the summer of 1986, V3.2 was frozen at the end ofNovember 1986. V3.4 was developed in the first half of 1987.

Thierry Coquand held a post-doctoral position in Cambridge Universityin 1986-87, where he developed a variant implementation in SML, withwhich he wrote some developments on fixpoints in Scott's domains.

Version 4¶

This version saw the beginning of program extraction from proofs, withtwo varieties of the type Prop of propositions, indicatingconstructive intent. The proof extraction algorithms were implementedby Christine Paulin-Mohring.

V4.1 was frozen on July 24th, 1987. It had a first identified libraryof mathematical developments (directory exemples), with librariesLogic (containing impredicative encodings of intuitionistic logic andalgebraic primitives for booleans, natural numbers and list), Peanodeveloping second-order Peano arithmetic, Arith defining addition,multiplication, euclidean division and factorial. Typical developmentswere the Knaster-Tarski theorem and Newman's lemma from rewritingtheory.

V4.2 was a joint development of a team consisting of Thierry Coquand,Gérard Huet and Christine Paulin-Mohring. A file V4.2.log records thelog of changes. It was frozen on September 1987 as the last versionimplemented in CAML 2.3, and V4.3 followed on CAML 2.5, a more stabledevelopment system.

V4.3 saw the first top-level of the system. Instead of evaluatingexplicit quotations, the user could develop his mathematics in ahigh-level language called the mathematical vernacular (followingAutomath terminology). The user could develop files in the vernacularnotation (with .v extension) which were now separate from the mlsources of the implementation. Gilles Dowek joined the team todevelop the vernacular language as his DEA internship research.

A notion of sticky constant was introduced, in order to keep names oflemmas when local hypotheses of proofs were discharged. This gave anotion of global mathematical environment with local sections.

Another significant practical change was that the system, originallydeveloped on the VAX central computer of our lab, was transferred onSUN personal workstations, allowing a level of distributeddevelopment. The extraction algorithm was modified, with threeannotations Pos, Null and Typ decorating the sorts Propand Type.

Version 4.3 was frozen at the end of November 1987, and wasdistributed to an early community of users (among those were HugoHerbelin and Loic Colson).

V4.4 saw the first version of (encoded) inductive types. Now naturalnumbers could be defined as:

[source, coq]Inductive NAT : Prop = O : NAT | Succ : NAT->NAT.

These inductive types were encoded impredicatively in the calculus,using a subsystem rec due to Christine Paulin. V4.4 was frozen onMarch 6th 1988.

Version 4.5 was the first one to support inductive types and programextraction. Its banner was Calcul des Constructions avecRéalisations et Synthèse. The vernacular language was enriched toaccommodate extraction commands.

The verification engine design was presented as: G. Huet. TheConstructive Engine. Version 4.5. Invited Conference, 2nd EuropeanSymposium on Programming, Nancy, March 88. The final paper,describing the V4.9 implementation, appeared in: A perspective inTheoretical Computer Science, Commemorative Volume in memory of GiftSiromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989.

Version 4.5 was demonstrated in June 1988 at the YoP Institute onLogical Foundations of Functional Programming organized by Gérard Huetat Austin, Texas.

Version 4.6 was started during the summer of 1988. Its mainimprovement was the complete rehaul of the proof synthesis engine byThierry Coquand, with a tree structure of goals.

Its source code was communicated to Randy Pollack on September 2nd1988. It evolved progressively into LEGO, proof system for Luo'sformalism of Extended Calculus of Constructions.

The discharge tactic was modified by Gérard Huet to allow forinter-dependencies in discharged lemmas. Christine Paulin improved theinductive definition scheme in order to accommodate predicates of anyarity.

Version 4.7 was started on September 6th, 1988.

This version starts exploiting the CAML notion of module in order toimprove the modularity of the implementation. Now the term verifier isidentified as a proper module Machine, which the structure of itsinternal data structures being hidden and thus accessible only throughthe legitimate operations. This machine (the constructive engine) wasthe trusted core of the implementation. The proof synthesis mechanismwas a separate proof term generator. Once a complete proof term wassynthesized with the help of tactics, it was entirely re-checked bythe engine. Thus there was no need to certify the tactics, and thesystem took advantage of this fact by having tactics ignore theuniverse levels, universe consistency check being relegated to thefinal type checking pass. This induced a certain puzzlement in earlyusers who saw, after a successful proof search, their QED followedby silence, followed by a failure message due to a universeinconsistency…

The set of examples comprise set theory experiments by Hugo Herbelin,and notably the Schroeder-Bernstein theorem.

Version 4.8, started on October 8th, 1988, saw a majorre-implementation of the abstract syntax type constr, separatingvariables of the formalism and metavariables denoting incomplete termsmanaged by the search mechanism. A notion of level (with three valuesTYPE, OBJECT and PROOF) is made explicit and a type judgementclarifies the constructions, whose implementation is now fullyexplicit. Structural equality is speeded up by using pointer equality,yielding spectacular improvements. Thierry Coquand adapts the proofsynthesis to the new representation, and simplifies pattern matchingto first-order predicate calculus matching, with important performancegain.

A new representation of the universe hierarchy is then defined byGérard Huet. Universe levels are now implemented implicitly, througha hidden graph of abstract levels constrained with an order relation.Checking acyclicity of the graph insures well-foundedness of theordering, and thus consistency. This was documented in a memo AddingType:Type to the Calculus of Constructions which was never published.

The development version is released as a stable 4.8 at the end of1988.

Version 4.9 is released on March 1st 1989, with the new "elastic"universe hierarchy.

The spring of 1989 saw the first attempt at documenting the systemusage, with a number of papers describing the formalism:

Metamathematical Investigations of a Calculus of Constructions, byThierry Coquand[Coq89],
Inductive definitions in the Calculus of Constructions, byChristine Paulin-Mohrin,
Extracting Fω's programs from proofs in the Calculus ofConstructions, by Christine Paulin-Mohring*[PM89],
The Constructive Engine, by Gérard Huet[Hue89],

as well as a number of user guides:

A short user's guide for the Constructions, Version 4.10, by Gérard Huet
A Vernacular Syllabus, by Gilles Dowek.
The Tactics Theorem Prover, User's guide, Version 4.10, by ThierryCoquand.

Stable V4.10, released on May 1st, 1989, was then a mature system,distributed with CAML V2.6.

In the mean time, Thierry Coquand and Christine Paulin-Mohring hadbeen investigating how to add native inductive types to the Calculusof Constructions, in the manner of Per Martin-Löf's IntuitionisticType Theory. The impredicative encoding had already been presented in:F. Pfenning and C. Paulin-Mohring. Inductively defined types in theCalculus of Constructions[PPM89]. An extension of the calculuswith primitive inductive types appeared in: T. Coquand andC. Paulin-Mohring. Inductively defined types[CP90].

This led to the Calculus of Inductive Constructions, logical formalismimplemented in Versions 5 upward of the system, and documented in:C. Paulin-Mohring. Inductive Definitions in the System Coq - Rulesand Properties[PM93b].

The last version of CONSTR is Version 4.11, which was last distributedin the spring of 1990. It was demonstrated at the first workshop ofthe European Basic Research Action Logical Frameworks In SophiaAntipolis in May 1990.

Version 5¶

At the end of 1989, Version 5.1 was started, and renamed as the systemCoq for the Calculus of Inductive Constructions. It was then ported tothe new stand-alone implementation of ML called Caml-light.

In 1990 many changes occurred. Thierry Coquand left for ChalmersUniversity in Göteborg. Christine Paulin-Mohring took a CNRSresearcher position at the LIP laboratory of École Normale Supérieurede Lyon. Project Formel was terminated, and gave rise to two teams:Cristal at INRIA-Roquencourt, that continued developments infunctional programming with Caml-light then OCaml, and Coq, continuingthe type theory research, with a joint team headed by Gérard Huet atINRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratoryof CNRS-ENS Lyon.

Chetan Murthy joined the team in 1991 and became the main softwarearchitect of Version 5. He completely rehauled the implementation forefficiency. Versions 5.6 and 5.8 were major distributed versions,with complete documentation and a library of users' developments. Theuse of the RCS revision control system, and systematic ChangeLogfiles, allow a more precise tracking of the software developments.

September 2015 +

Thierry Coquand, Gérard Huet and Christine Paulin-Mohring.

Versions 6¶

Version 6.1¶

The present version 6.1 of Coq is based on the V5.10 architecture. Itwas ported to the new language Objective Caml by Bruno Barras. Theunderlying framework has slightly changed and allows more conversionsbetween sorts.

The new version provides powerful tools for easier developments.

Cristina Cornes designed an extension of the Coq syntax to allowdefinition of terms using a powerful pattern matching analysis in thestyle of ML programs.

Amokrane Saïbi wrote a mechanism to simulate inheritance between typesfamilies extending a proposal by Peter Aczel. He also developed amechanism to automatically compute which arguments of a constant may beinferred by the system and consequently do not need to be explicitlywritten.

Yann Coscoy designed a command which explains a proof term using naturallanguage. Pierre Crégut built a new tactic which solves problems inquantifier-free Presburger Arithmetic. Both functionalities have beenintegrated to the Coq system by Hugo Herbelin.

Samuel Boutin designed a tactic for simplification of commutative ringsusing a canonical set of rewriting rules and equality moduloassociativity and commutativity.

Finally the organisation of the Coq distribution has been supervised byJean-Christophe Filliâtre with the help of Judicaël Courant and BrunoBarras.

Lyon, Nov. 18th 1996

Christine Paulin

Version 6.2¶

In version 6.2 of Coq, the parsing is done using camlp4, a preprocessorand pretty-printer for CAML designed by Daniel de Rauglaudre at INRIA.Daniel de Rauglaudre made the first adaptation of Coq for camlp4, thiswork was continued by Bruno Barras who also changed the structure of Coqabstract syntax trees and the primitives to manipulate them. The resultof these changes is a faster parsing procedure with greatly improvedsyntax-error messages. The user-interface to introduce grammar orpretty-printing rules has also changed.

Eduardo Giménez redesigned the internal tactic libraries, giving uniformnames to Caml functions corresponding to Coq tactic names.

Bruno Barras wrote new, more efficient reduction functions.

Hugo Herbelin introduced more uniform notations in the Coq specificationlanguage: the definitions by fixpoints and pattern matching have a morereadable syntax. Patrick Loiseleur introduced user-friendly notationsfor arithmetic expressions.

New tactics were introduced: Eduardo Giménez improved the mechanism tointroduce macros for tactics, and designed special tactics for(co)inductive definitions; Patrick Loiseleur designed a tactic tosimplify polynomial expressions in an arbitrary commutative ring whichgeneralizes the previous tactic implemented by Samuel Boutin.Jean-Christophe Filliâtre introduced a tactic for refining a goal, usinga proof term with holes as a proof scheme.

David Delahaye designed the tool to search an object in the librarygiven its type (up to isomorphism).

Henri Laulhère produced the Coq distribution for the Windowsenvironment.

Finally, Hugo Herbelin was the main coordinator of the Coq documentationwith principal contributions by Bruno Barras, David Delahaye,Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin and PatrickLoiseleur.

Orsay, May 4th 1998

Christine Paulin

Version 6.3¶

The main changes in version V6.3 were the introduction of a few newtactics and the extension of the guard condition for fixpointdefinitions.

Versions 7¶

Summary of changes¶

The version V7 is a new implementation started in September 1999 byJean-Christophe Filliâtre. This is a major revision with respect to theinternal architecture of the system. The Coq version 7.0 was distributedin March 2001, version 7.1 in September 2001, version 7.2 in January2002, version 7.3 in May 2002 and version 7.4 in February 2003.

Jean-Christophe Filliâtre designed the architecture of the new system.He introduced a new representation for environments and wrote a newkernel for type checking terms. His approach was to use functionaldata-structures in order to get more sharing, to prepare the addition ofmodules and also to get closer to a certified kernel.

Hugo Herbelin introduced a new structure of terms with localdefinitions. He introduced “qualified” names, wrote a newpattern matching compilation algorithm and designed a more compactalgorithm for checking the logical consistency of universes. Hecontributed to the simplification of Coq internal structures and theoptimisation of the system. He added basic tactics for forward reasoningand coercions in patterns.

David Delahaye introduced a new language for tactics. General tacticsusing pattern matching on goals and context can directly be written fromthe Coq toplevel. He also provided primitives for the design ofuser-defined tactics in Caml.

Micaela Mayero contributed the library on real numbers. OlivierDesmettre extended this library with axiomatic trigonometric functions,square, square roots, finite sums, Chasles property and basic planegeometry.

Jean-Christophe Filliâtre and Pierre Letouzey redesigned a newextraction procedure from Coq terms to Caml or Haskell programs. Thisnew extraction procedure, unlike the one implemented in previous versionof Coq is able to handle all terms in the Calculus of InductiveConstructions, even involving universes and strong elimination. P.Letouzey adapted user contributions to extract ML programs when it wassensible. Jean-Christophe Filliâtre wrote coqdoc, a documentationtool for Coq libraries usable from version 7.2.

Bruno Barras improved the efficiency of the reduction algorithm and theconfidence level in the correctness of Coq critical type checkingalgorithm.

Yves Bertot designed the SearchPattern and SearchRewrite toolsand the support for the pcoq interface(http://www-sop.inria.fr/lemme/pcoq/).

Micaela Mayero and David Delahaye introduced Field, a decision tacticfor commutative fields.

Christine Paulin changed the elimination rules for empty and singletonpropositional inductive types.

Loïc Pottier developed Fourier, a tactic solving linear inequalities onreal numbers.

Pierre Crégut developed a new, reflection-based version of the Omegadecision procedure.

Claudio Sacerdoti Coen designed an XML output for the Coq modules to beused in the Hypertextual Electronic Library of Mathematics (HELM cfhttp://www.cs.unibo.it/helm).

A library for efficient representation of finite maps using binary treescontributed by Jean Goubault was integrated in the basic theories.

Pierre Courtieu developed a command and a tactic to reason on theinductive structure of recursively defined functions.

Jacek Chrząszcz designed and implemented the module system of Coq whosefoundations are in Judicaël Courant’s PhD thesis.

The development was coordinated by C. Paulin.

Many discussions within the Démons team and the LogiCal projectinfluenced significantly the design of Coq especially with J. Courant,J. Duprat, J. Goubault, A. Miquel, C. Marché, B. Monate and B. Werner.

Intensive users suggested improvements of the system : Y. Bertot, L.Pottier, L. Théry, P. Zimmerman from INRIA, C. Alvarado, P. Crégut,J.-F. Monin from France Telecom R & D.

Orsay, May. 2002

Hugo Herbelin & Christine Paulin

Details of changes in 7.0 and 7.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 7.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 basename, the name of the module in which they are defined (Top if incoqtop), and possibly an arbitrary long sequence of directory (e.g."Coq.Lists.PolyList.flat_map" where "Coq" means that "flat_map" is partof Coq standard library, "Lists" means it is defined in the Listslibrary and "PolyList" means it is in the file Polylist) (+)
Constructions can be referred by their base name, or, in case ofconflict, by a "qualified" name, where the base name is prefixedby the module name (and possibly by a directory name, and soon). A fully qualified name is an absolute name which always referto the construction it denotes (to preserve the visibility ofall constructions, no conflict is allowed for an absolute name) (+)
Long names are available for modules with the possibility of usingthe directory name as a component of the module full name (withoption -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 (mainsource 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 andFact's now survive at the end of section, but are only accessible using aqualified names as soon as their strength expires; Local's disappear andare moved into local definitions for each construction persistent atsection 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 oflocal 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 becometransparent (a constant intended to be alternatively opaque andtransparent must be declared as transparent (using Defined)); a riskexists (until next Coq version) that Simpl and Hnf reduces opaqueconstants (*)

New tactics¶

New set of tactics to deal with types equipped with specificequalities (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 Elimand Induction, Case and Destruct in a more user-friendly way (seerestrictions 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 Ltaclanguage; they run faster and produce more compact proofs; Tauto isfully compatible but, in exchange of a better uniformity, Intuitionis slightly weaker (then use Tauto instead) (**)(+)
New tactic Field to decide equalities on commutative fields (as aspecial 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 onthe types of local definitions
Inversion, Injection, Discriminate, ... apply also on thequantified 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 formt=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 theprimitive "let-in" (+)
Elim can no longer be used with an elimination schema different fromthe one defined at definition time of the inductive type. To overloadan elimination schema, use "Elim <hyp> using <name of the new schema>"(*)(+)
Simpl no longer unfolds the recursive calls of a mutually definedfixpoint (*)(+)
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 ofHint Rewrite to deal with generated subgoals (+)
Redundant or incompatible instantiations in Apply ... with ... are nowcorrectly 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 stillsupported but it is not advised to use them) (*)(+)
Entry "command" in "Grammar" and quotations (<<...>> stuff) isrenamed "constr" as in "Syntax" (+)
New syntax "[" sentence_1 ... sentence_n"]." to group sentences (usefulfor Time and to write grammar rules abbreviating several commands) (+)
The default parser for actions in the grammar rules (and forpatterns in the pretty-printing rules) is now the one associated withthe grammar (i.e. vernac, tactic or constr); no need then forquotations as in <:vernac:<...>>; to return an "ast", the grammarmust be explicitly typed with tag ": ast" or ": ast list", or if asyntax rule, by using <<...>> in the patterns (expression insidethese angle brackets are parsed as "ast"); for grammars other thanvernac, tactic or constr, you may explicitly type the action withtags ": 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 tooverloaded names (+)

New commands¶

New commands "Print XML All", "Show XML Proof", ... to show orexport theories to XML to be used with Helm's publishing and renderingtools (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 tacticlanguage 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 tacticsand 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 themodule 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 LoadPathPrint LoadPath -> Print LoadPathDelPath -> Remove LoadPathAddRecPath -> Add Rec LoadPathPrint Path -> Print Coercion Paths
Implicit Arguments On -> Set Implicit ArgumentsImplicit Arguments Off -> Unset Implicit Arguments
Begin Silent -> Set SilentEnd 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 logicalone (+)
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] (CarlosDaniel Luna,Montevideo)
Specification and verification of the Railroad Crossing Problemin 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 editiondistance algorithm [Diff] (Jean-Christophe Filliâtre, Orsay)
Correctness proofs of Buchberger's algorithm [Buchberger] and RSAcryptographic algorithm [Rsa] (Laurent Théry, Sophia-Antipolis)
Correctness proof of Stalmarck tautology checker algorithm[Stalmarck] (Laurent Théry, Pierre Letouzey, Sophia-Antipolis)

Details of changes in 7.2¶

Language

Automatic insertion of patterns for local definitions in the type ofthe constructors of an inductive types (for compatibility with V6.3let-in style)
Coercions allowed in Cases patterns
New declaration "Canonical Structure id = t : I" to help resolution ofequations of the form (proj ?)=a; if proj(e)=a then a is canonicallyequipped 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 plugins/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-recursiveplus 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 andtrigonometric functions (R_sqr.v - Rtrigo.v); a complementary approachand new theorems about continuity and derivability in Ranalysis.v; someproperties in plane geometry such as translation, rotation or similarityin 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.txtfor a description of the main changes in the interface files of V7.2)
New behavior of Intuition/Tauto may exceptionally lead to incompatibilities

Details of changes in 7.3¶

Language

Slightly improved compilation of pattern-matching (slight source ofincompatibilities)
Record's now accept anonymous fields "_" which does not build projections
Changes in the allowed elimination sorts for certain class of inductivedefinitions : an inductive definition without constructorsof Sort Prop can be eliminated on sorts Set and Type A "singleton"inductive definition (one constructor with arguments in the sort Proplike conjunction of two propositions or equality) can be eliminateddirectly 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 butbetter applies congruence laws of plus (slight source of incompatibilities).
Field now accepts terms to be simplified as arguments (as for Ring). Thisextension has been also implemented using the toplevel tactic language.
Intuition does no longer unfold constants except "<->" and "~". Itcan be parameterized by a tactic. It also can introduce dependentproduct if needed (source of incompatibilities)
"Match Context" now matching more recent hypotheses first and failing onlyon 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 (sourceof 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 plugins/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.vand Zlogarithms.v) moved from plugins/omega in order to be morevisible, one Zsgn function, more induction principles (Wf_Z.v andtail 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 thenew 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 overrational 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 datatypeZChinese is the new version, Chinese the obsolete one[Pierre Letouzey, LRI Orsay]

Incompatibilities

Ring: exceptional incompatibilities (1 above 650 in submitted usercontribs, 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 ofsubmitted user contributions necessitating the removal of now superfluousproof steps in 3 different proofs)
Match Context, in case of incompatibilities because of a now nontrapped error (e.g. Not_found or Failure), use instead tactic Failto force Match Context trying the next clause
Inversion: better simplification and discrimination may occasionallylead to less subgoals and/or hypotheses and different naming of hypotheses
Unification done by Apply/Elim has been changed and may exceptionally leadto incompatible instantiations
Peano_dec.v and Compare_dec.v parts of Arith.v make Auto morepowerful if these files were not already required (1 occurrence ofthis in submitted user contribs)

Changes in 7.3.1¶

Bug fixes

Corrupted Field tactic and Match Context tactic construction fixed
Checking of names already existing in Assert added (#1386)
Invalid argument bug in Exact tactic solved (#1387)
Colliding bound names bug fixed (#1412)
Wrong non-recursivity test for Record fixed (#1394)
Out of memory/seg fault bug related to parametric inductive fixed (#1404)
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 andLetTac (#1402)

Details of changes in 7.4¶

Symbolic notations

Introduction of a notion of scope gathering notations in a consistent set;a notation sets has been developed for nat, Z and R (undocumented)
New command "Notation" for declaring notations simultaneously forparsing and printing (see chap 10 of the reference manual)
Declarations with only implicit arguments now handled (e.g. theargument of nil can be set implicit; use !nil to refer to nilwithout arguments)
"Print Scope sc" and "Locate ntn" allows to know to what expression anotation is bound
New defensive strategy for printing or not implicit arguments to ensurere-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 onlyallowed grammar types are constr and pattern; ast and ast list are nolonger supported; some incompatibilities in Grammar: when a syntax is ainitial 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 ofincompatibilities.
Syntactic Definitions Fst, Snd, Ex, All, Ex2, AllT, ExT, ExT2,ProjS1, ProjS2, Error, Value and Except are turned tonotations. They now must be applied (incompatibilities only inunrealistic 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 andRCompute. 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 declarethe corresponding constructor as a coercion.
Idem for assumptions declarations and constants when the type is mentioned.
The "Coercion" and "Canonical Structure" keywords now accept thesame 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: whensections are closed, the full name of a Remark or a Fact has no longer asection part (source of incompatibilities)
Opaque Local's (i.e. built by tactics and ended by Qed), do notsurvive section closing any longer; as a side-effect, Opaque Local'snow appear in the local context of proofs; their body is hiddenthough (source of incompatibilities); use one of Remark/Fact/Lemma/Theoreminstead to simulate the old behavior of Local (the section part ofthe name is not kept though)

ML tactics and commands

"Grammar tactic" and "Grammar vernac" of type "ast" are no longersupported (only "Grammar tactic simple_tactic" of type "tactic"remains available).
Concrete syntax for ML written commands and tactics isnow declared at ML level using camlp4 macros TACTIC EXTEND et VERNACCOMMAND 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 ofincompatibilities, especially, Recursive keyword is required formutually recursive definitions).
New evaluation semantics: no more partial evaluation at definition time;evaluation of all Tactic/Meta Definition, even producing terms, expecta 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) nowunderstand 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 asfor 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 thehypothesis was unfolded to x < y -> False. This is fixed. In addition,it can also recognize 'False' in the hypothesis and use it to solve thegoal.
Coercions now handled in "with" bindings
"Subst x" replaces all occurrences of x by t in the goal and hypotheseswhen an hypothesis x=t or x:=t or t=x exists
Fresh names for Assert and Pose now based on collision-avoidingIntro naming strategy (exceptional source of incompatibilities)
LinearIntuition (no documentation)
Unfold expects a correct evaluable argument
Clear expects existing hypotheses

Extraction (See details in plugins/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 nowincludes 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 ofsymbolic notations
Two new variants of implicit arguments are available
- Unset/Set Contextual Implicits tells to consider implicit also thearguments inferable from the context (e.g. for nil or refl_eq)
- Unset/Set Strict Implicits tells to consider implicit only thearguments that are inferable in any case (i.e. arguments that occursas 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 whenapplied to a predicate which does not use its argument)

Incompatibilities

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

Bugs

Improved localisation of errors in Syntactic Definitions
Induction principle creation failure in presence of let-in fixed (#1459)
Inversion bugs fixed (#1427 and #1437)
Omega bug related to Set fixed (#1384)
Type-checking inefficiency of nested destructuring let-in fixed (#1435)
Improved handling of let-in during holes resolution phase (#1460)

Efficiency

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