From 6e1c88226eb2ab188a1aaaf9a31667967c85fc65 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 2 Oct 2015 16:32:20 +0200 Subject: Update the history of versions with recent versions. --- dev/doc/versions-history.tex | 50 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 9892a4419f..fab6a37ef4 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -265,7 +265,17 @@ Coq V7.3.1& released 5 October 2002 & \feature{module system} [2-8-2002]\\ & & \feature{pattern-matching compilation} (version 2) [13-6-2002]\\ Coq V7.4& released 6 February 2003 & \feature{notation}, \feature{scopes} [13-10-2002]\\ +\end{tabular} +\medskip +\bigskip + +\centerline{V- New concrete syntax} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline Coq V8.0& released 21 April 2004 & \feature{new concrete syntax}, \feature{Set predicative}, \feature{CoqIDE} [from 4-2-2003]\\ Coq V8.0pl1& released 18 July 2004\\ @@ -307,6 +317,46 @@ Coq V8.2 & released 17 February 2009 & \feature{type classes} [10-12-2007], \fea & & a first package released on February 11 was incomplete\\ +Coq V8.2pl1& released 4 July 2009 & \\ +Coq V8.2pl2& released 29 June 2010 & \\ +\end{tabular} + +\medskip +\bigskip + +\newpage +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +Coq V8.3 beta & released 16 February 2010 & \feature{MSets library} [13-10-2009] \\ +Coq V8.3 & released 14 October 2010 & \feature{nsatz} [3-6-2010] \\ +Coq V8.3pl1& released 23 December 2010 & \\ +Coq V8.3pl2& released 19 April 2011 & \\ +Coq V8.3pl3& released 19 December 2011 & \\ +Coq V8.3pl3& released 26 March 2012 & \\ +Coq V8.3pl5& released 28 September 2012 & \\ +Coq V8.4 beta & released 27 December 2011 & \feature{modular arithmetic library} [2010-2012]\\ +&& \feature{vector library} [10-12-2010]\\ +&& \feature{structured scripts} [22-4-2010]\\ +&& \feature{eta-conversion} [20-9-2010]\\ +&& \feature{new proof engine available} [10-12-2010]\\ +Coq V8.4 beta2 & released 21 May 2012 & \\ +Coq V8.4 & released 12 August 2012 &\\ +Coq V8.4pl1& released 22 December 2012 & \\ +Coq V8.4pl2& released 4 April 2013 & \\ +Coq V8.4pl3& released 21 December 2013 & \\ +Coq V8.4pl4& released 24 April 2014 & \\ +Coq V8.4pl5& released 22 October 2014 & \\ +Coq V8.4pl6& released 9 April 2015 & \\ + +Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation to OCaml} [22-1-2013]\\ +&& \feature{asynchonous evaluation} [8-8-2013]\\ +&& \feature{new proof engine deployed} [2-11-2013]\\ +&& \feature{universe polymorphism} [6-5-2014]\\ +&& \feature{primitive projections} [6-5-2014]\\ + +Coq V8.5 beta2 & released 22 April 2015 & \feature{MMaps library} [4-3-2015]\\ + \end{tabular} \medskip -- cgit v1.2.3 From 9227d6e9412ae4ebe70fb9b6bd5d2f6ecc354864 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 1 Oct 2015 09:29:10 +0200 Subject: Improving reference manual in that auto uses simple apply rather than apply. Still, there are small differences, e.g. on "use_metas_eagerly_in_conv_on_closed_terms", but also maybe in some amount of use of delta that Matthieu would know better than me if it matters or not in practice. --- doc/refman/RefMan-tac.tex | 51 ++++++++++++++++++++++++++--------------------- 1 file changed, 28 insertions(+), 23 deletions(-) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index fa6f783934..06431055ad 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3394,7 +3394,7 @@ local definition. Example: {\tt unfold not in (Type of H1) (Type of H3).} This tactic implements a Prolog-like resolution procedure to solve the current goal. It first tries to solve the goal using the {\tt assumption} tactic, then it reduces the goal to an atomic one using -{\tt intros} and introducing the newly generated hypotheses as hints. +{\tt intros} and introduces the newly generated hypotheses as hints. Then it looks at the list of tactics associated to the head symbol of the goal and tries to apply one of them (starting from the tactics with lower cost). This process is recursively applied to the generated @@ -3454,11 +3454,10 @@ intact. \texttt{auto} and \texttt{trivial} never fail. \tacindex{eauto} \label{eauto} -This tactic generalizes {\tt auto}. In contrast with -the latter, {\tt eauto} uses unification of the goal -against the hints rather than pattern-matching -(in other words, it uses {\tt eapply} instead of -{\tt apply}). +This tactic generalizes {\tt auto}. While {\tt auto} does not try +resolution hints which would leave existential variables in the goal, +{\tt eauto} does try them (informally speaking, it uses {\tt eapply} +where {\tt auto} uses {\tt apply}). As a consequence, {\tt eauto} can solve such a goal: \begin{coq_eval} @@ -3623,21 +3622,27 @@ The {\hintdef} is one of the following expressions: \item {\tt Resolve \term} \comindex{Hint Resolve} - This command adds {\tt apply {\term}} to the hint list + This command adds {\tt simple apply {\term}} to the hint list with the head symbol of the type of \term. The cost of that hint is - the number of subgoals generated by {\tt apply {\term}}. - - In case the inferred type of \term\ does not start with a product the - tactic added in the hint list is {\tt exact {\term}}. In case this - type can be reduced to a type starting with a product, the tactic {\tt - apply {\term}} is also stored in the hints list. - - If the inferred type of \term\ contains a dependent - quantification on a predicate, it is added to the hint list of {\tt - eapply} instead of the hint list of {\tt apply}. In this case, a - warning is printed since the hint is only used by the tactic {\tt - eauto} (see \ref{eauto}). A typical example of a hint that is used - only by \texttt{eauto} is a transitivity lemma. + the number of subgoals generated by {\tt simple apply {\term}}. +%{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false + + The cost of that hint is the number of subgoals generated by that + tactic. + + % Is it really needed? + %% In case the inferred type of \term\ does not start with a product + %% the tactic added in the hint list is {\tt exact {\term}}. In case + %% this type can however be reduced to a type starting with a product, + %% the tactic {\tt apply {\term}} is also stored in the hints list. + + If the inferred type of \term\ contains a dependent quantification + on a variable which occurs only in the premisses of the type and not + in its conclusion, no instance could be inferred for the variable by + unification with the goal. In this case, the hint is added to the + hint list of {\tt eauto} (see \ref{eauto}) instead of the hint list + of {\tt auto} and a warning is printed. A typical example of a hint + that is used only by \texttt{eauto} is a transitivity lemma. \begin{ErrMsgs} \item \errindex{Bound head variable} @@ -3649,7 +3654,7 @@ The {\hintdef} is one of the following expressions: The type of {\term} contains products over variables that do not appear in the conclusion. A typical example is a transitivity axiom. - In that case the {\tt apply} tactic fails, and thus is useless. + In that case the {\tt simple apply} tactic fails, and thus is useless. \end{ErrMsgs} @@ -3664,10 +3669,10 @@ The {\hintdef} is one of the following expressions: \item \texttt{Immediate {\term}} \comindex{Hint Immediate} - This command adds {\tt apply {\term}; trivial} to the hint list + This command adds {\tt simple apply {\term}; trivial} to the hint list associated with the head symbol of the type of {\ident} in the given database. This tactic will fail if all the subgoals generated by - {\tt apply {\term}} are not solved immediately by the {\tt trivial} + {\tt simple apply {\term}} are not solved immediately by the {\tt trivial} tactic (which only tries tactics with cost $0$). This command is useful for theorems such as the symmetry of equality -- cgit v1.2.3 From 5e62675419fb6a5a8f8a86fbf3f6df4427e70d21 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 2 Oct 2015 16:50:26 +0200 Subject: Fixing error messages about Hint. --- doc/refman/RefMan-tac.tex | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 06431055ad..a21e5631fc 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3645,16 +3645,16 @@ The {\hintdef} is one of the following expressions: that is used only by \texttt{eauto} is a transitivity lemma. \begin{ErrMsgs} - \item \errindex{Bound head variable} +%% \item \errindex{Bound head variable} + + \item \term\ \errindex{cannot be used as a hint} The head symbol of the type of {\term} is a bound variable such that this tactic cannot be associated to a constant. - \item \term\ \errindex{cannot be used as a hint} - - The type of {\term} contains products over variables that do not - appear in the conclusion. A typical example is a transitivity axiom. - In that case the {\tt simple apply} tactic fails, and thus is useless. + %% The type of {\term} contains products over variables that do not + %% appear in the conclusion. A typical example is a transitivity axiom. + %% In that case the {\tt simple apply} tactic fails, and thus is useless. \end{ErrMsgs} @@ -3684,7 +3684,7 @@ The {\hintdef} is one of the following expressions: \begin{ErrMsgs} - \item \errindex{Bound head variable} +%% \item \errindex{Bound head variable} \item \term\ \errindex{cannot be used as a hint} @@ -3710,7 +3710,9 @@ The {\hintdef} is one of the following expressions: \item {\ident} \errindex{is not an inductive type} - \item {\ident} \errindex{not declared} +% No need to have this message here, is is generic to all commands +% referring to globals +%% \item {\ident} \errindex{not declared} \end{ErrMsgs} -- cgit v1.2.3 From beedccef9ddc8633c705d7c5ee2f1bbbb3ec8a47 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 2 Oct 2015 17:43:32 +0200 Subject: Updating versions history with data from Gérard. Adding Gérard's history file about V1-V5 versions. --- dev/doc/README-V1-V5 | 293 +++++++++++++++++++++++++++++++++++++++++++ dev/doc/versions-history.tex | 59 ++++++--- 2 files changed, 333 insertions(+), 19 deletions(-) create mode 100644 dev/doc/README-V1-V5 diff --git a/dev/doc/README-V1-V5 b/dev/doc/README-V1-V5 new file mode 100644 index 0000000000..2ca62e3d74 --- /dev/null +++ b/dev/doc/README-V1-V5 @@ -0,0 +1,293 @@ + + Notes on the prehistory of Coq + +This archive contains the sources of the CONSTR ancestor of the Coq proof +assistant. CONSTR, then Coq, was designed and implemented in the Formel team, +joint between the INRIA Rocquencourt laboratory and the Ecole Normale Supérieure +of Paris, from 1984 onwards. + +Version 1 + +This software is a prototype type-checker for a higher-order logical formalism +known as the Theory of Constructions, presented in his PhD thesis by +Thierry Coquand, with influences from Girard's system F and de Bruijn's Automath. +The metamathematical analysis of the system is the +PhD work of Thierry Coquand. The software is mostly the work of Gérard Huet. +Most of the mathematical examples verified with the software are due +to Thierry Coquand. + +The programming language of the CONSTR software (as it was called at the time) +is a version of ML issued from the Edinburgh LCF system and running on +a LISP backend. The main improvements from the original LCF ML are that ML +is compiled rather than interpreted (Gérard Huet building on the original +translator by Lockwood Morris), and that it is enriched by recursively +defined types (work of Guy Cousineau). This ancestor of CAML was used +and improved by Larry Paulson for his implementation of Cambridge LCF. + +Software developments of this prototype occurred from late 1983 to early 1985. + +Version 1.10 was frozen on December 22nd 1984. It is the version used for the +examples in Thierry Coquand's thesis, defended on January 31st 1985. +There was a unique binding operator, used both for universal quantification +(dependent product) at the level of types and functional abstraction (lambda) +at the level of terms/proofs, in the manner of Automath. Substitution +(lambda reduction) was implemented using de Bruijn's indexes. + +Version 1.11 was frozen on February 19th, 1985. It is the version used for the +examples in the paper: +Th. Coquand, G. Huet. Constructions: A Higher Order Proof System for Mechanizing +Mathematics. Invited paper, EUROCAL85, April 1985, Linz, Austria. Springer Verlag +LNCS 203, pp. 151-184. + +Christine Paulin joined the team at this point, for her DEA research internship. +In her DEA memoir (August 1985) she presents developments for the lambo function +computing 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", was presented +with a proof of consistency and comparisons with proof systems of Per +Martin Löf, Girard, and the Automath family of N. de Bruijn, in the paper: +T. Coquand and G. Huet. The Calculus of Constructions. +Submitted on June 30th 1985, accepted on December 5th, 1985, +Information and Computation. Preprint as Rapport de Recherche Inria n°530, +Mai 1986. Final version in Information and Computation 76,2/3, Feb. 88. + +An abstraction of the software design, in the form of an abstract machine +for proof checking, and a fuller sequence of mathematical developments was +presented in: +Th. Coquand, G. Huet. Concepts Mathématiques et Informatiques Formalisés dans le Calcul des Constructions. Invited paper, European Logic Colloquium, Orsay, +July 1985. Preprint as Rapport de recherche INRIA n°463, Dec. 85. +Published in Logic Colloquium 1985, North-Holland, 1987. + +Version 2.8 was frozen on December 16th, 1985, and served for developing +the exemples in the above papers. + +This calculus was then enriched in version 2.9 with a cumulative hierarchy of +universes. Universe levels were initially explicit natural numbers. +Another improvement was the possibility of automatic synthesis of implicit +type arguments, relieving the user of tedious redundant declarations. + +Christine Paulin wrote an article "Algorithm development in the Calculus of +Constructions", preprint as Rapport de recherche INRIA n°497, March 86. +Final version in Proceedings Symposium on Logic in Computer Science, Cambridge, +MA, 1986 (IEEE Computer Society Press). Besides lambo and majority, +she presents quicksort and a text formatting algorithm. + +Version 2.13 of the calculus of constructions with universes was frozen +on June 25th, 1986. + +A synthetic presentation of type theory along constructive lines with ML +algorithms was given by Gérard Huet in his May 1986 CMU course notes +"Formal Structures for Computation and Deduction". Its chapter +"Induction and Recursion in the Theory of Constructions" was presented +as an invited paper at the Joint Conference on Theory and Practice of Software +Development TAPSOFT’87 at Pise in March 1987, and published as +"Induction Principles Formalized in the Calculus of Constructions" in +Programming of Future Generation Computers, Ed. K. Fuchi and M. Nivat, +North-Holland, 1988. + +Version 3 + +This version saw the beginning of proof automation, with a search algorithm +inspired from PROLOG and the applicative logic programming programs +of the course notes "Formal structures for computation and deduction". +The search algorithm was implemented in ML by Thierry Coquand. +The proof system could thus be used in two modes: proof verification and +proof synthesis, with tactics such as "AUTO". + +The implementation language was now called CAML, for "categorical abstract +machine language". It used as backend the LLM3 virtual machine of Le Lisp +by Jérôme Chailloux. The main developers of CAML were Michel Mauny, +Ascander Suarez and Pierre Weis. + +V3.1 was started in the summer of 1986, V3.2 was frozen at the end of November +1986. V3.4 was developed in the first half of 1987. + +Thierry Coquand held a post-doctoral position in Cambrige University in 1986-87, +where he developed a variant implementation in SML, with which he wrote +some developments on fixpoints in Scott's domains. + +Version 4 + +This version saw the beginning of program extraction from proofs, with +two varieties of the type Prop of propositions, indicating constructive intent. +The proof extraction algorithms were implemented by Christine Paulin-Mohring. + +V4.1 was frozen on July 24th, 1987. It had a first identified library of +mathematical developments (directory exemples), with libraries Logic +(containing impredicative encodings of intuitionistic logic and algebraic +primitives for booleans, natural numbers and list), Peano developing second-order +Peano arithmetic, Arith defining addition, multiplication, euclidean division +and factorial. Typical developments were the Knaster-Tarski theorem +and Newman's lemma from rewriting theory. + +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 the log of changes. +It was frozen on September 1987 as the last version implemented in CAML 2.3, +and V4.3 followed on CAML 2.5, a more stable development system. + +V4.3 saw the first top-level of the system. Instead of evaluating explicit +quotations, the user could develop his mathematics in a high-level language +called the mathematical vernacular (following Automath terminology). +The user could develop files in the vernacular notation (with .v extension) +which were now separate from the ml sources of the implementation. +Gilles Dowek joined the team to develop the vernacular language as his +DEA internship research. + +A notion of sticky constant was introduced, in order to keep names of lemmas +when local hypotheses of proofs were discharged. This gave a notion +of global mathematical environment with local sections. + +Another significant practical change was that the system, originally developped +on the VAX central computer of our lab, was transferred on SUN personal +workstations, allowing a level of distributed development. +The extraction algorithm was modified, with three annotations Pos, Null and +Typ decorating the sorts Prop and Type. + +Version 4.3 was frozen at the end of November 1987, and was distributed to an +early community of users (among those were Hugo Herbelin and Loic Colson). + +V4.4 saw the first version of (encoded) inductive types. +Now natural numbers could be defined as: +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 on March 6th 1988. + +Version 4.5 was the first one to support inductive types and program extraction. +Its banner was "Calcul des Constructions avec Realisations et Synthese". +The vernacular language was enriched to accommodate extraction commands. + +The verification engine design was presented as: +G. Huet. The Constructive Engine. Version 4.5. Invited Conference, 2nd European +Symposium on Programming, Nancy, March 88. +The final paper, describing the V4.9 implementation, appeared in: +A perspective in Theoretical Computer Science, Commemorative Volume in memory +of Gift Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989. + +Version 4.5 was demonstrated in June 1988 at the YoP Institute on Logical +Foundations of Functional Programming organized by Gérard Huet at Austin, Texas. + +Version 4.6 was started during summer 1988. Its main improvement was the +complete rehaul of the proof synthesis engine by Thierry Coquand, with +a tree structure of goals. + +Its source code was communicated to Randy Pollack on September 2nd 1988. +It evolved progressively into LEGO, proof system for Luo's formalism +of Extended Calculus of Constructions. + +The discharge tactic was modified by G. Huet to allow for inter-dependencies +in discharged lemmas. Christine Paulin improved the inductive definition scheme +in order to accommodate predicates of any arity. + +Version 4.7 was started on September 6th, 1988. + +This version starts exploiting the CAML notion of module in order to improve the +modularity of the implementation. Now the term verifier is identified as +a proper module Machine, which the structure of its internal data structures +being hidden and thus accessible only through the legitimate operations. +This machine (the constructive engine) was the trusted core of the +implementation. The proof synthesis mechanism was a separate proof term +generator. Once a complete proof term was synthesized with the help of tactics, +it was entirely re-checked by the engine. Thus there was no need to certify +the tactics, and the system took advantage of this fact by having tactics ignore +the universe levels, universe consistency check being relegated to the final +type-checking pass. This induced a certain puzzlement of early users who saw +their successful proof search ended with QED, followed by silence, followed by +a failure message of universe inconsistency rejection... + +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 major re-implementation of the +abstract syntax type constr, separating variables of the formalism and +metavariables denoting incomplete terms managed by the search mechanism. +A notion of level (with three values TYPE, OBJECT and PROOF) is made explicit +and a type judgement clarifies the constructions, whose implementation is now +fully explicit. Structural equality is speeded up by using pointer equality, +yielding spectacular improvements. Thierry Coquand adapts the proof synthesis +to the new representation, and simplifies pattern matching to 1st order +predicate calculus matching, with important performance gain. + +A new representation of the universe hierarchy is then defined by G. Huet. +Universe levels are now implemented implicitly, through a hidden graph +of abstract levels constrained with an order relation. +Checking acyclicity of the graph insures well-foundedness of the ordering, +and thus consistency. This was documented in a memo +"Adding Type:Type to the Calculus of Constructions" which was never published. + +The development version is released as a stable 4.8 at the end of 1988. + +Version 4.9 is released on March 1st 1989, with the new "elastic" +universe hierarchy. + +The spring 89 saw the first attempt at documenting the system usage, +with a number of papers describing the formalism: +- Metamathematical Investigations of a Calculus of Constructions, by +Thierry Coquand (INRIA Research Report N°1088, Sept. 1989, published in +Logic and Computer Science, ed. P.G. Odifreddi, Academic Press, 1990) +- Inductive definitions in the Calculus of Constructions, by +Christine Paulin-Mohring, +- Extracting Fomega's programs from proofs in the Calculus of Constructions, by +Christine Paulin-Mohring (published in POPL'89) +- The Constructive Engine, by Gérard Huet +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 Thierry Coquand. + +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 +had been investigating how to add native inductive types to the +Calculus of Constructions, in the manner of Per Martin-Löf's Intuitionistic +Type Theory. The impredicative encoding had already been presented in: +F. Pfenning and C. Paulin-Mohring. Inductively defined types in the Calculus +of Constructions. Preprint technical report CMU-CS-89-209, final version in +Proceedings of Mathematical Foundations of Programming Semantics, +volume 442, Lecture Notes in Computer Science. Springer-Verlag, 1990. +An extension of the calculus with primitive inductive types appeared in: +Th. Coquand and C. Paulin-Mohring. Inductively defined types. +In P. Martin-Löf and G. Mints, editors, Proceedings of Colog'88, volume 417, +Lecture Notes in Computer Science. Springer-Verlag, 1990. + +This lead to the Calculus of Inductive Constructions, logical formalism +implemented in Versions 5 upward of the system, and documented in: +C. Paulin-Mohring. Inductive Definitions in the System Coq - Rules and +Properties. In M. Bezem and J.-F. Groote, editors, Proceedings of the conference +Typed Lambda Calculi and Applications, volume 664, Lecture Notes in Computer +Science, 1993. + +The last version of CONSTR is Version 4.11, which was last distributed +in Spring 1990. It was demonstrated at the first workshop of the European +Basic Research Action Logical Frameworks In Sophia Antipolis in May 1990. + +At the end of 1989, Version 5.1 was started, and renamed as the system Coq +for the Calculus of Inductive Constructions. It was then ported to the new +stand-alone implementation of ML called Caml-light. + +In 1990 many changes occurred. Thierry Coquand left for Chalmers University +in Göteborg. Christine Paulin-Mohring took a CNRS researcher position +at the LIP laboratory of Ecole Normale Supérieure de Lyon. Project Formel +was terminated, and gave rise to two teams: Cristal at INRIA-Roquencourt, +that continued developments in functional programming with Caml-light then +Ocaml, and Coq, continuing the type theory research, with a joint team +headed by Gérard Huet at INRIA-Rocquencourt and Christine Paulin-Mohring +at the LIP laboratory of CNRS-ENS Lyon. + +Chetan Murthy joined the team in 1991 and became the main software architect +of Version 5. He completely rehauled the implementation for efficiency. +Versions 5.6 and 5.8 were major distributed versions, with complete +documentation and a library of users' developements. The use of the RCS +revision control system, and systematic ChangeLog files, allow a more +precise tracking of the software developments. + +Developments from Version 6 upwards are documented in the credits section of +Coq's Reference Manual. + +September 2015 +Thierry Coquand, Gérard Huet and Christine Paulin-Mohring. diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index fab6a37ef4..1b1d3500a4 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -10,55 +10,76 @@ \begin{center} \begin{huge} -An history of Coq versions +A history of Coq versions \end{huge} \end{center} \bigskip \centerline{\large 1984-1989: The Calculus of Constructions} + +\bigskip +\centerline{\large (see README.V1-V5 for details)} \mbox{}\\ \mbox{}\\ \begin{tabular}{l|l|l} version & date & comments \\ \hline -CoC V1.10& mention of dates from 6 December & implementation language is Caml\\ - & 1984 to 13 February 1985 \\ -CoC V1.11& mention of dates from 6 December\\ - & 1984 to 19 February 1985\\ +CONSTR V1.10& mention of dates from 6 December & \feature{type-checker for Coquand's Calculus }\\ + & 1984 to 13 February 1985 & \feature{of Constructions}, implementation \\ + & frozen 22 December 1984 & language is a predecessor of CAML\\ + +CONSTR V1.11& mention of dates from 6 December\\ + & 1984 to 19 February 1985 (freeze date) &\\ + +CoC V2.8& dated 16 December 1985 (freeze date)\\ -CoC V2.13& dated 16 December 1985\\ +CoC V2.9& & \feature{cumulative hierarchy of universes}\\ -CoC V2.13& dated 25 June 1986\\ +CoC V2.13& dated 25 June 1986 (freeze date)\\ -CoC V3.1& dated 20 November 1986 & \feature{auto}\\ +CoC V3.1& started summer 1986 & \feature{AUTO tactic}\\ + & dated 20 November 1986 & implementation language now named CAML\\ CoC V3.2& dated 27 November 1986\\ -CoC V3.3 and V3.4& dated 1 January 1987 & creation of a directory for examples\\ +CoC V3.3& dated 1 January 1987 & creation of a directory for examples\\ -CoC V4.1& dated 24 July 1987\\ +CoC V3.4& dated 1 January 1987 & \feature{lambda and product distinguished in the syntax}\\ + +CoC V4.1& dated 24 July 1987 (freeze date)\\ CoC V4.2& dated 10 September 1987\\ -CoC V4.3& dated 15 September 1987\\ +CoC V4.3& dated 15 September 1987 & \feature{mathematical vernacular toplevel}\\ + & frozen November 1987 & \feature{section mechanism}\\ + & & \feature{logical vs computational content (sorte Spec)}\\ + & & \feature{LCF engine}\\ + +CoC V4.4& dated 27 January 1988 & \feature{impredicatively encoded inductive types}\\ + & frozen March 1988\\ -CoC V4.4& dated 27 January 1988\\ +CoC V4.5 and V4.5.5& dated 15 March 1988 & \feature{program extraction}\\ + & demonstrated in June 1988\\ -CoC V4.5 and V4.5.5& dated 15 March 1988\\ +CoC V4.6& dated 1 September 1988 & start of LEGO fork\\ -CoC V4.6 and V4.7& dated 1 September 1988\\ +CoC V4.7& started 6 September 1988 \\ -CoC V4.8& dated 1 December 1988\\ +CoC V4.8& dated 1 December 1988 (release time) & \feature{floating universes}\\ -CoC V4.8.5& dated 1 February 1989\\ +CoC V4.8.5& dated 1 February 1989 & \\ -CoC V4.9& dated 1 March 1989\\ +CoC V4.9& dated 1 March 1989 (release date)\\ -CoC V4.10 and 4.10.1& dated 1 May 1989 & first public release - in English\\ +CoC V4.10 and 4.10.1& dated 1 May 1989 & released with documentation in English\\ \end{tabular} \bigskip + +\noindent Note: CoC above stands as an abbreviation for {\em Calculus of + Constructions}, official name of the system. +\bigskip \bigskip \newpage @@ -80,7 +101,7 @@ Coq V5.2 & log dated 4 October 1990 & internal use \\ Coq V5.3 & log dated 12 October 1990 & internal use \\ -Coq V5.4 & headers dated 24 October 1990 & internal use, \feature{extraction} (version 1) [3-12-90]\\ +Coq V5.4 & headers dated 24 October 1990 & internal use, new \feature{extraction} (version 1) [3-12-90]\\ Coq V5.5 & started 6 December 1990 & internal use \\ -- cgit v1.2.3 From f41de34bcd48f008cf7d3fae4c7fce925048e606 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 2 Oct 2015 21:32:25 +0200 Subject: Mark the Coq.Compat files for documentation. (Fix bug #4353) --- doc/stdlib/index-list.html.template | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 024e13413a..866193ffb4 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -591,7 +591,7 @@ through the Require Import command.

Program: - Support for dependently-typed programming. + Support for dependently-typed programming
theories/Program/Basics.v @@ -612,4 +612,12 @@ through the Require Import command.

theories/Unicode/Utf8_core.v theories/Unicode/Utf8.v
+ +
Compat: + Compatibility wrappers for previous versions of Coq +
+
+ theories/Compat/Coq84.v + theories/Compat/Coq85.v +
-- cgit v1.2.3 From 2b033589d1b7900fdb86dfad145f1c284657ae8c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 4 Oct 2015 09:22:16 +0200 Subject: Fix typo. (Fix bug #4355) --- doc/refman/RefMan-oth.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 739a89af4c..4b2b8660c2 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -967,8 +967,8 @@ the constants {\qualid$_1$} {\ldots} {\qualid$_n$} in tactics using $\delta$-conversion (unfolding a constant is replacing it by its definition). -{\tt Opaque} has also on effect on the conversion algorithm of {\Coq}, -telling it to delay the unfolding of a constant as mush as possible when +{\tt Opaque} has also an effect on the conversion algorithm of {\Coq}, +telling it to delay the unfolding of a constant as much as possible when {\Coq} has to check the conversion (see Section~\ref{conv-rules}) of two distinct applied constants. -- cgit v1.2.3 From 6f51b8cafe7a873600e7a0c8675a72a8aee40184 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 5 Oct 2015 10:29:37 +0200 Subject: Univs: fix handling of evar_map in identity coercion construction. --- toplevel/class.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/toplevel/class.ml b/toplevel/class.ml index 0e270f960b..f925a2d07e 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -186,8 +186,9 @@ let error_not_transparent source = let build_id_coercion idf_opt source poly = let env = Global.env () in - let vs, ctx = match source with - | CL_CONST sp -> Universes.fresh_global_instance env (ConstRef sp) + let sigma = Evd.from_env env in + let sigma, vs = match source with + | CL_CONST sp -> Evd.fresh_global env sigma (ConstRef sp) | _ -> error_not_transparent source in let c = match constant_opt_value_in env (destConst vs) with | Some c -> c @@ -208,8 +209,8 @@ let build_id_coercion idf_opt source poly = (* juste pour verification *) let _ = if not - (Reductionops.is_conv_leq env Evd.empty - (Typing.unsafe_type_of env Evd.empty val_f) typ_f) + (Reductionops.is_conv_leq env sigma + (Typing.unsafe_type_of env sigma val_f) typ_f) then errorlabstrm "" (strbrk "Cannot be defined as coercion (maybe a bad number of arguments).") @@ -218,13 +219,13 @@ let build_id_coercion idf_opt source poly = match idf_opt with | Some idf -> idf | None -> - let cl,u,_ = find_class_type Evd.empty t in + let cl,u,_ = find_class_type sigma t in Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - (definition_entry ~types:typ_f ~poly ~univs:(Univ.ContextSet.to_context ctx) + (definition_entry ~types:typ_f ~poly ~univs:(Evd.universe_context sigma) ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in let decl = (constr_entry, IsDefinition IdentityCoercion) in -- cgit v1.2.3 From bba2cfb5921653f18d6cedf2800cdc1abf9310af Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 5 Oct 2015 16:34:57 +0200 Subject: Update the .mailmap file. The update process is as follows: run "git shortlog -s -e" and look for duplicate or missing contributors. --- .mailmap | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/.mailmap b/.mailmap index 7223b7354a..13c71558f0 100644 --- a/.mailmap +++ b/.mailmap @@ -9,47 +9,47 @@ ## If you're mentionned here and want to update your information, ## either amend this file and commit it, or contact the coqdev list +Jim Apple jbapple Bruno Barras barras Bruno Barras barras-local Yves Bertot bertot -Yves Bertot Yves Bertot Frédéric Besson fbesson Pierre Boutillier pboutill Pierre Boutillier Pierre Pierre Boutillier Pierre Boutillier Xavier Clerc xclerc Xavier Clerc xclerc -Pierre Corbineau corbinea +Pierre Corbineau corbinea Judicaël Courant courant Pierre Courtieu courtieu -# uncapitalises the email address: -Pierre Courtieu Pierre Courtieu David Delahaye delahaye Maxime Dénès mdenes Daniel De Rauglaudre ddr Olivier Desmettre desmettr Damien Doligez doligez -Jean-Christophe Filliâtre filliatr +Jean-Christophe Filliâtre filliatr +Jean-Christophe Filliâtre Jean-Christophe Filliatre Julien Forest jforest Julien Forest forest Julien Forest jforest +Julien Forest jforest Stéphane Glondu glondu -# corrects accent: Stéphane Glondu Stephane Glondu -Benjamin Grégoire bgregoir -Benjamin Grégoire gregoire +Benjamin Grégoire Benjamin Gregoire +Benjamin Grégoire bgregoir +Benjamin Grégoire gregoire Jason Gross Jason Gross +Jason Gross Jason Gross Vincent Gross vgross Huang Guan-Shieng huang Hugo Herbelin herbelin -# uncapitalises the email address: -Hugo Herbelin Hugo Herbelin Tom Hutchinson thutchin Cezary Kaliszyk cek Florent Kirchner fkirchne Florent Kirchner kirchner +Marc Lasson mlasson Pierre Letouzey letouzey -Assia Mahboubi amahboub +Assia Mahboubi amahboub Evgeny Makarov emakarov Gregory Malecha Gregory Malecha Lionel Elie Mamane lmamane @@ -68,7 +68,7 @@ Christine Paulin mohring ppedrot Loïc Pottier pottier Matthias Puech puech -Yann Régis-Gianas regisgia +Yann Régis-Gianas regisgia Clément Renard clrenard Claudio Sacerdoti Coen sacerdot Vincent Siles vsiles @@ -77,8 +77,7 @@ Matthieu Sozeau msozeau Matthieu Sozeau Arnaud Spiwack aspiwack Enrico Tassi gareuselesinge -# uncapitalizes the email address -Enrico Tassi Enrico Tassi +Enrico Tassi Enrico Tassi Enrico Tassi Enrico Tassi Laurent Théry thery Benjamin Werner werner -- cgit v1.2.3 From 92ee78086f1ca89646ac69a00256ff45fcaee22c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 5 Oct 2015 17:00:11 +0200 Subject: Univs: fix printing bug #3797. --- printing/printmod.ml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/printing/printmod.ml b/printing/printmod.ml index a80bbb146a..53d0508c7f 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -259,6 +259,10 @@ let print_body is_impl env mp (l,body) = | SFBmodule _ -> keyword "Module" ++ spc () ++ name | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name | SFBconst cb -> + let u = + if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + else Univ.Instance.empty + in (match cb.const_body with | Def _ -> def "Definition" ++ spc () | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () @@ -268,14 +272,16 @@ let print_body is_impl env mp (l,body) = | Some env -> str " :" ++ spc () ++ hov 0 (Printer.pr_ltype_env env Evd.empty (* No evars in modules *) - (Typeops.type_of_constant_type env cb.const_type)) ++ + (Vars.subst_instance_constr u + (Typeops.type_of_constant_type env cb.const_type))) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env Evd.empty (Mod_subst.force_constr l)) + Printer.pr_lconstr_env env Evd.empty + (Vars.subst_instance_constr u (Mod_subst.force_constr l))) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx cb.const_universes) + Printer.pr_universe_ctx (Univ.instantiate_univ_context cb.const_universes)) | SFBmind mib -> try let env = Option.get env in -- cgit v1.2.3 From efce61af32ff1b09a21dcf88bca7d6609a0bfd27 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 5 Oct 2015 17:22:31 +0200 Subject: Univs: fix bug #4288, Print Sorted generated backward < constraints. --- kernel/univ.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kernel/univ.ml b/kernel/univ.ml index 73d323426b..34eb283d73 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1582,8 +1582,8 @@ let sort_universes orig = let sorted = LMap.fold fold compact UMap.empty in (** Add all [Type.n] nodes *) let fold i accu u = - if 0 < i then - let pred = types.(i - 1) in + if i < max then + let pred = types.(i + 1) in let arc = {univ = u; lt = [pred]; le = []; rank = 0; status = Unset; } in UMap.add u (Canonical arc) accu else accu -- cgit v1.2.3 From 07f4e6b07775052cc1c5dc34cdfa7ad4eacfa94f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 4 Oct 2015 14:50:45 +0200 Subject: Fix bug #4354: interpret hints in the right env and sigma. --- pretyping/evd.ml | 5 ++++- tactics/auto.ml | 7 +++++-- tactics/class_tactics.ml | 6 +++--- tactics/eauto.ml4 | 5 +++-- tactics/hints.ml | 23 ++++++++++++----------- tactics/hints.mli | 4 ++-- test-suite/bugs/closed/4354.v | 10 ++++++++++ 7 files changed, 39 insertions(+), 21 deletions(-) create mode 100644 test-suite/bugs/closed/4354.v diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 842b87c57e..4e0b6f75e7 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -312,7 +312,10 @@ let union_evar_universe_context ctx ctx' = let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) (Univ.ContextSet.levels ctx.uctx_local) in - let declarenew g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g in + let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in + let declarenew g = + Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g + in let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); uctx_local = local; diff --git a/tactics/auto.ml b/tactics/auto.ml index 72ba9e0bd9..e5fdf6a7c2 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -309,7 +309,8 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in let hyp = Context.map_named_declaration nf decl in let hintl = make_resolve_hyp env sigma hyp - in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db) + in trivial_fail_db dbg mod_delta db_list + (Hint_db.add_list env sigma hintl local_db) end) in Proofview.Goal.enter begin fun gl -> @@ -438,7 +439,9 @@ let possible_resolve dbg mod_delta db_list local_db cl = with Not_found -> [] let extend_local_db decl db gl = - Hint_db.add_list (make_resolve_hyp (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) decl) db + let env = Tacmach.New.pf_env gl in + let sigma = Proofview.Goal.sigma gl in + Hint_db.add_list env sigma (make_resolve_hyp env sigma decl) db (* Introduce an hypothesis, then call the continuation tactic [kont] with the hint db extended with the so-obtained hypothesis *) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 80f47c680f..ed5b783f6c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -190,7 +190,7 @@ let rec e_trivial_fail_db db_list local_db goal = let d = pf_last_hyp g' in let hintl = make_resolve_hyp (pf_env g') (project g') d in (e_trivial_fail_db db_list - (Hint_db.add_list hintl local_db) g'))) :: + (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) :: (List.map (fun (x,_,_,_,_) -> x) (e_trivial_resolve db_list local_db (project goal) (pf_concl goal))) in @@ -339,7 +339,7 @@ let make_hints g st only_classes sign = (PathOr (paths, path), hint @ hints) else (paths, hints)) (PathEmpty, []) sign - in Hint_db.add_list hintlist (Hint_db.empty st true) + in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true) let make_autogoal_hints = let cache = ref (true, Environ.empty_named_context_val, @@ -374,7 +374,7 @@ let intro_tac : atac = let context = Environ.named_context_of_val (Goal.V82.hyps s g') in let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints) (true,false,false) info.only_classes None (List.hd context) in - let ldb = Hint_db.add_list hint info.hints in + let ldb = Hint_db.add_list env s hint info.hints in (g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls in {it = gls'; sigma = s;}) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 34f87c6cf0..83498cabd8 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -147,7 +147,7 @@ let rec e_trivial_fail_db db_list local_db goal = let d = pf_last_hyp g' in let hintl = make_resolve_hyp (pf_env g') (project g') d in (e_trivial_fail_db db_list - (Hint_db.add_list hintl local_db) g'))) :: + (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) :: (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) ) in tclFIRST (List.map tclCOMPLETE tacl) goal @@ -269,7 +269,8 @@ module SearchProblem = struct let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') in - let ldb = Hint_db.add_list hintl (List.hd s.localdb) in + let ldb = Hint_db.add_list (pf_env g') (project g') + hintl (List.hd s.localdb) in { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp; dblist = s.dblist; localdb = ldb :: List.tl s.localdb; prev = ps }) diff --git a/tactics/hints.ml b/tactics/hints.ml index a7eae667d0..dbb2340364 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -266,11 +266,10 @@ let strip_params env c = | _ -> c) | _ -> c -let instantiate_hint p = +let instantiate_hint env sigma p = let mk_clenv c cty ctx = - let env = Global.env () in - let sigma = Evd.merge_context_set univ_flexible (Evd.from_env env) ctx in - let cl = mk_clenv_from_env (Global.env()) sigma None (c,cty) in + let sigma = Evd.merge_context_set univ_flexible sigma ctx in + let cl = mk_clenv_from_env env sigma None (c,cty) in {cl with templval = { cl.templval with rebus = strip_params env cl.templval.rebus }; env = empty_env} @@ -524,8 +523,8 @@ module Hint_db = struct in List.fold_left (fun db (gr,(id,v)) -> addkv gr id v db) db' db.hintdb_nopat - let add_one (k, v) db = - let v = instantiate_hint v in + let add_one env sigma (k, v) db = + let v = instantiate_hint env sigma v in let st',db,rebuild = match v.code.obj with | Unfold_nth egr -> @@ -542,7 +541,7 @@ module Hint_db = struct let db, id = next_hint_id db in addkv k id v db - let add_list l db = List.fold_left (fun db k -> add_one k db) db l + let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l let remove_sdl p sdl = List.smartfilter p sdl @@ -812,7 +811,9 @@ let add_hint dbname hintlist = in let () = List.iter check hintlist in let db = get_db dbname in - let db' = Hint_db.add_list hintlist db in + let env = Global.env () in + let sigma = Evd.from_env env in + let db' = Hint_db.add_list env sigma hintlist db in searchtable_add (dbname,db') let add_transparency dbname grs b = @@ -1166,8 +1167,8 @@ let expand_constructor_hints env sigma lems = let add_hint_lemmas env sigma eapply lems hint_db = let lems = expand_constructor_hints env sigma lems in let hintlist' = - List.map_append (make_resolves env sigma (eapply,true,false) None true) lems in - Hint_db.add_list hintlist' hint_db + List.map_append (make_resolves env sigma (eapply,true,false) None false) lems in + Hint_db.add_list env sigma hintlist' hint_db let make_local_hint_db env sigma ts eapply lems = let sign = Environ.named_context env in @@ -1177,7 +1178,7 @@ let make_local_hint_db env sigma ts eapply lems = in let hintlist = List.map_append (make_resolve_hyp env sigma) sign in add_hint_lemmas env sigma eapply lems - (Hint_db.add_list hintlist (Hint_db.empty ts false)) + (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false)) let make_local_hint_db = if Flags.profile then diff --git a/tactics/hints.mli b/tactics/hints.mli index 687bc78c76..5a4fb77091 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -93,8 +93,8 @@ module Hint_db : arguments. *) val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list - val add_one : hint_entry -> t -> t - val add_list : (hint_entry) list -> t -> t + val add_one : env -> evar_map -> hint_entry -> t -> t + val add_list : env -> evar_map -> hint_entry list -> t -> t val remove_one : global_reference -> t -> t val remove_list : global_reference list -> t -> t val iter : (global_reference option -> bool array list -> full_hint list -> unit) -> t -> unit diff --git a/test-suite/bugs/closed/4354.v b/test-suite/bugs/closed/4354.v new file mode 100644 index 0000000000..6a2f9672d3 --- /dev/null +++ b/test-suite/bugs/closed/4354.v @@ -0,0 +1,10 @@ +Inductive True : Prop := I. +Class Lift (T : Type). +Axiom closed_increment : forall {T} {H : Lift T}, True. +Create HintDb core. +Lemma closed_monotonic T (H : Lift T) : True. + auto using closed_increment. Show Universes. +Qed. + +(* also fails with -nois, so the content of the hint database does not matter +*) \ No newline at end of file -- cgit v1.2.3 From df9caebb04fb681ec66b79c41ae01918cd2336de Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 6 Oct 2015 09:58:20 +0200 Subject: Univs (pretyping): call vm_compute/native_compute with the current universe graph --- pretyping/pretyping.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f18657da82..2efd8fe413 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -903,7 +903,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in if not (occur_existential cty || occur_existential tval) then begin - try + try + let env = Environ.push_context_set (Evd.universe_context_set !evdref) env in ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj with Reduction.NotConvertible -> error_actual_type_loc loc env !evdref cj tval @@ -915,6 +916,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in let evars = Nativenorm.evars_of_evar_map !evdref in + let env = Environ.push_context_set (Evd.universe_context_set !evdref) env in begin try ignore (Nativeconv.native_conv Reduction.CUMUL evars env cty tval); cj -- cgit v1.2.3 From 840155eafd9607c7656c80770de1e2819fe56a13 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 6 Oct 2015 13:38:15 +0200 Subject: Fixing emacs output in debugging mode. Goal displaying during Debugging ltac is a notice message now. Other messages are debug messages. This does not change anything in coqide or coqtop, but allows proofgeneral to dispatch them in the right buffers (pg had to be fixed too). --- proofs/logic_monad.ml | 6 +++++- proofs/logic_monad.mli | 4 ++++ proofs/tactic_debug.ml | 5 +++-- 3 files changed, 12 insertions(+), 3 deletions(-) diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml index cb3e5a1860..81f02b66db 100644 --- a/proofs/logic_monad.ml +++ b/proofs/logic_monad.ml @@ -95,7 +95,11 @@ struct let print_char = fun c -> (); fun () -> print_char c (** {!Pp.pp}. The buffer is also flushed. *) - let print = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e -> + let print_debug = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e -> + let (e, info) = Errors.push e in raise ~info e () + + (** {!Pp.pp}. The buffer is also flushed. *) + let print = fun s -> (); fun () -> try Pp.msg_notice s; Pp.pp_flush () with e -> let (e, info) = Errors.push e in raise ~info e () let timeout = fun n t -> (); fun () -> diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli index ab729aff71..511dd7a6ed 100644 --- a/proofs/logic_monad.mli +++ b/proofs/logic_monad.mli @@ -58,6 +58,10 @@ module NonLogical : sig (** {!Pp.pp}. The buffer is also flushed. *) val print : Pp.std_ppcmds -> unit t + (* FIXME: shouldn't we have a logger instead? *) + (** {!Pp.pp}. The buffer is also flushed. *) + val print_debug : Pp.std_ppcmds -> unit t + (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) val raise : ?info:Exninfo.info -> exn -> 'a t diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index d7f4b5ead5..667765dbf2 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -32,7 +32,8 @@ let explain_logic_error = ref (fun e -> mt()) let explain_logic_error_no_anomaly = ref (fun e -> mt()) -let msg_tac_debug s = Proofview.NonLogical.print (s++fnl()) +let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl()) +let msg_tac_notice s = Proofview.NonLogical.print (s++fnl()) (* Prints the goal *) @@ -48,7 +49,7 @@ let db_pr_goal gl = let db_pr_goal = Proofview.Goal.nf_enter begin fun gl -> let pg = db_pr_goal gl in - Proofview.tclLIFT (msg_tac_debug (str "Goal:" ++ fnl () ++ pg)) + Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg)) end -- cgit v1.2.3