diff options
| -rw-r--r-- | doc/AddRefMan-pre.tex | 18 | ||||
| -rw-r--r-- | doc/Cases.tex | 48 | ||||
| -rwxr-xr-x | doc/Extraction.tex | 48 | ||||
| -rw-r--r-- | doc/Polynom.tex | 28 | ||||
| -rwxr-xr-x | doc/RefMan-int.tex | 48 | ||||
| -rwxr-xr-x | doc/RefMan-pre.tex | 100 | ||||
| -rwxr-xr-x | doc/macros.tex | 3 |
7 files changed, 152 insertions, 141 deletions
diff --git a/doc/AddRefMan-pre.tex b/doc/AddRefMan-pre.tex index 3ddf2e0c5..bd661aeef 100644 --- a/doc/AddRefMan-pre.tex +++ b/doc/AddRefMan-pre.tex @@ -9,21 +9,21 @@ Here you will find several pieces of additional documentation for the \Coq\ Reference Manual. Each of this chapters is concentrated on a particular topic, that should interest only a fraction of the \Coq\ -users : that's the reason why they are apart from the Reference +users: that's the reason why they are apart from the Reference Manual. \begin{description} \item[Extended pattern-matching] This chapter details the use of generalized pattern-matching. It is contributed by Cristina Cornes - and Hugo Herbelin + and Hugo Herbelin. \item[Implicit coercions] This chapter details the use of the coercion mechanism. It is contributed by Amokrane Saïbi. -\item[Proof of imperative programs] This chapter explains how to - prove properties of annotated programs with imperative features. - It is contributed by Jean-Christophe Filliâtre +%\item[Proof of imperative programs] This chapter explains how to +% prove properties of annotated programs with imperative features. +% It is contributed by Jean-Christophe Filliâtre \item[Program extraction] This chapter explains how to extract in practice ML files from $\FW$ terms. It is contributed by Jean-Christophe @@ -36,10 +36,10 @@ Manual. \item[Omega] \texttt{Omega}, written by Pierre Crégut, solves a whole class of arithmetic problems. -\item[Program] The \texttt{Program} technology intends to inverse the - extraction mechanism. It allows the developments of certified - programs in \Coq. This chapter is due to Catherine Parent. {\bf This - feature is not available in {\Coq} version 7.} +%\item[Program] The \texttt{Program} technology intends to inverse the +% extraction mechanism. It allows the developments of certified +% programs in \Coq. This chapter is due to Catherine Parent. {\bf This +% feature is not available in {\Coq} version 7.} \item[The {\tt Ring} tactic] This is a tactic to do AC rewriting. This chapter explains how to use it and how it works. diff --git a/doc/Cases.tex b/doc/Cases.tex index 06dd10d7d..11e20d110 100644 --- a/doc/Cases.tex +++ b/doc/Cases.tex @@ -35,7 +35,8 @@ Notice also that the annotation is mandatory when the sequence of equation is empty. \begin{figure}[t] -\fbox{\parbox{\linewidth}{ +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} \begin{tabular}{rcl} {\nestedpattern} & := & {\ident} \\ & $|$ & \_ \\ @@ -55,7 +56,8 @@ empty. \zeroone{\annotation} \texttt{Cases} \nelist{\term}{} \texttt{of} \sequence{\exteqn}{$|$} \texttt{end} \\ \end{tabular} -}} +\end{minipage}} +\end{center} \caption{Extended Cases syntax} \label{cases-grammar} \end{figure} @@ -584,35 +586,33 @@ generated expression and the original. Here is a summary of the error messages corresponding to each situation: -\begin{itemize} -\item patterns are incorrect (because constructors are not applied to - the correct number of the arguments, because they are not linear or - they are wrongly typed) -\begin{itemize} +\begin{ErrMsgs} \item \sverb{The constructor } {\sl ident} \sverb{expects } {\sl num} \sverb{arguments} -\item \sverb{The variable } {\sl ident} \sverb{is bound several times + \sverb{The variable } {\sl ident} \sverb{is bound several times in pattern } {\sl term} -\item \sverb{Found a constructor of inductive type} {\term} + \sverb{Found a constructor of inductive type} {\term} \sverb{while a constructor of} {\term} \sverb{is expected} -\end{itemize} -\item the pattern matching is not exhaustive -\begin{itemize} -\item \sverb{Non exhaustive pattern-matching} -\end{itemize} -\item the elimination predicate provided to \texttt{Cases} has not the - expected arity + Patterns are incorrect (because constructors are not applied to + the correct number of the arguments, because they are not linear or + they are wrongly typed) + +\item \errindex{Non exhaustive pattern-matching} + +the pattern matching is not exhaustive -\begin{itemize} \item \sverb{The elimination predicate } {\sl term} \sverb{should be of arity } {\sl num} \sverb{(for non dependent case) or } {\sl num} \sverb{(for dependent case)} -\end{itemize} -\item the whole expression is wrongly typed +The elimination predicate provided to \texttt{Cases} has not the + expected arity + + +%\item the whole expression is wrongly typed % CADUC ? % , or the synthesis of @@ -627,13 +627,11 @@ Here is a summary of the error messages corresponding to each situation: % recommend the user to rewrite the nested dependent patterns into % several \texttt{Cases} with {\em simple patterns}. -\item there is a type mismatch between the different branches - - \begin{itemize} - \item {\tt Unable to infer a Cases predicate\\ +\item {\tt Unable to infer a Cases predicate\\ Either there is a type incompatiblity or the problem involves\\ dependencies} - \end{itemize} + + There is a type mismatch between the different branches Then the user should provide an elimination predicate. @@ -713,7 +711,7 @@ Here is a summary of the error messages corresponding to each situation: % end. % \end{coq_example} -\end{itemize} +\end{ErrMsgs} %%% Local Variables: diff --git a/doc/Extraction.tex b/doc/Extraction.tex index 2ef5c41c1..12a9616e2 100755 --- a/doc/Extraction.tex +++ b/doc/Extraction.tex @@ -580,39 +580,42 @@ quite efficient for Caml code. As a test, we propose an automatic extraction of the Standard Library of \Coq. In particular, we will find back the two previous examples, {\tt Euclid} and {\tt Heapsort}. -Go to directory\\ -{\tt contrib/extraction/test} of the sources of \Coq, and run commands:\\ - -\mbox{\tt make tree; make}\\ - +Go to directory {\tt contrib/extraction/test} of the sources of \Coq, +and run commands: +\begin{verbatim} +make tree; make +\end{verbatim} This will extract all Standard Library files and compile them. It is done via many {\tt Extraction Module}, with some customization (see subdirectory {\tt custom}). The result of this extraction of the Standard Library can be browsed -at the address:\\ - -\verb!http://www.lri.fr/~letouzey/extraction!\\ - +at URL +\begin{flushleft} +\url{http://www.lri.fr/~letouzey/extraction}. +\end{flushleft} + %Reals theory is normally not extracted, since it is an axiomatic %development. We propose nonetheless a dummy realization of those %axioms, to test, run: \\ % %\mbox{\tt make reals}\\ -This test works also with Haskell. In the same directory, run: \\ - -\mbox{\tt make tree; make -f Makefile.haskell}\\ - -The haskell compiler currently used is {\tt hbc}. -Any other should also work, just -adapt the {\tt Makefile.haskell}. In particular {\tt ghc} is known -to work. +This test works also with Haskell. In the same directory, run: +\begin{verbatim} +make tree; make -f Makefile.haskell +\end{verbatim} +The haskell compiler currently used is {\tt hbc}. Any other should +also work, just adapt the {\tt Makefile.haskell}. In particular {\tt + ghc} is known to work. \asubsection{Extraction's horror museum} - Some pathological examples of extraction are grouped in the file\\ - {\tt contrib/extraction/test\_extraction.v} of the sources of \Coq. +Some pathological examples of extraction are grouped in the file +\begin{verbatim} +contrib/extraction/test_extraction.v +\end{verbatim} +of the sources of \Coq. \asubsection{Users' Contributions} @@ -643,6 +646,11 @@ to work. the only examples of developments where {\tt Obj.magic} are needed. This is probably due to an heavy use of impredicativity. After compilation those two examples run nonetheless, - thanks to the correction of the extraction (see \cite{Let02}). + thanks to the correction of the extraction~\cite{Let02}. % $Id$ + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: diff --git a/doc/Polynom.tex b/doc/Polynom.tex index d8d16b18a..d12781392 100644 --- a/doc/Polynom.tex +++ b/doc/Polynom.tex @@ -126,14 +126,17 @@ and $term_2$ will have the same associated variable number. \begin{ErrMsgs} \item \errindex{All terms must have the same type} \item \errindex{Don't know what to do with this goal} -\item \errindex{No Declared Ring Theory for \term.}\\ - \texttt{Use Add [Semi] Ring to declare it}\\ +\item \errindex{No Declared Ring Theory for \term.} + + \texttt{Use Add [Semi] Ring to declare it} + That happens when all terms have the same type \term, but there is no declared ring theory for this set. See below. \end{ErrMsgs} \begin{Variants} -\item \texttt{Ring}\\ +\item \texttt{Ring} + That works if the current goal is an equality between two polynomials. It will normalize both sides of the equality, solve it if the normal forms are equal and in other cases @@ -266,15 +269,17 @@ and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)}, \begin{Variants} \item \texttt{Add Semi Ring} \textit{A Aplus Amult Aone Azero Aeq T} \texttt{[} \textit{c1 \dots\ cn} \texttt{].}\comindex{Add Semi - Ring}\\ - There are two differences with the \texttt{Add Ring} command: - there is no inverse function and the term $T$ must be of type + Ring} + + There are two differences with the \texttt{Add Ring} command: there + is no inverse function and the term $T$ must be of type \texttt{(Semi\_Ring\_Theory }\textit{A Aplus Amult Aone Azero - Aeq}\texttt{)}. + Aeq}\texttt{)}. \item \texttt{Add Abstract Ring} \textit{A Aplus Amult Aone Azero Ainv - Aeq T}\texttt{.}\comindex{Add Abstract Ring}\\ - This command should be used for when the operations of rings are not + Aeq T}\texttt{.}\comindex{Add Abstract Ring} + + This command should be used for when the operations of rings are not computable; for example the real numbers of \texttt{theories/REALS/}. Here $0+1$ is not beta-reduced to $1$ but you still may want to \textit{rewrite} it to $1$ using the ring @@ -282,12 +287,13 @@ and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)}, that function is \verb+[x:A]false+. \item \texttt{Add Abstract Semi Ring} \textit{A Aplus Amult Aone Azero - Aeq T}\texttt{.}\comindex{Add Abstract Semi Ring}\\ + Aeq T}\texttt{.}\comindex{Add Abstract Semi Ring} \end{Variants} \begin{ErrMsgs} -\item \errindex{Not a valid (semi)ring theory}.\\ +\item \errindex{Not a valid (semi)ring theory}. + That happens when the typing condition does not hold. \end{ErrMsgs} diff --git a/doc/RefMan-int.tex b/doc/RefMan-int.tex index ee4be7560..9bcf2de77 100755 --- a/doc/RefMan-int.tex +++ b/doc/RefMan-int.tex @@ -58,37 +58,37 @@ below. \begin{itemize} \item The first part describes the specification language, - Gallina. The chapters \ref{Gallina} and \ref{Gallina-extension} + Gallina. Chapters~\ref{Gallina} and~\ref{Gallina-extension} describe the concrete syntax as well as the meaning of programs, - theorems and proofs in the Calculus of Inductive Constructions. The - chapter \ref{Theories} describes the standard library of \Coq. The - chapter \ref{Cic} is a mathematical description of the - formalism. The chapter \ref{Modules} describes the module system. + theorems and proofs in the Calculus of Inductive + Constructions. Chapter~\ref{Theories} describes the standard library + of \Coq. Chapter~\ref{Cic} is a mathematical description of the + formalism. Chapter~\ref{Modules} describes the module system. \item The second part describes the proof engine. It is divided in - for chapters. Chapter \ref{Vernacular-commands} presents - all commands (we call them \textit{vernacular commands}) that are not + four chapters. Chapter~\ref{Vernacular-commands} presents + all commands (we call them \emph{vernacular commands}) that are not directly related to interactive proving: requests to the environment, complete or partial evaluation, loading and compiling files. How to start and stop proofs, do multiple proofs in parallel is explained - in the chapter \ref{Proof-handling}. In chapter \ref{Tactics}, + in Chapter~\ref{Proof-handling}. In Chapter~\ref{Tactics}, all commands that realize one or more steps of the proof are - presented: we call them \textit{tactics}. Examples of tactics are - described in chapter~\ref{Tactics-examples}. + presented: we call them \emph{tactics}. Examples of tactics are + described in Chapter~\ref{Tactics-examples}. \item The third part describes how to extend the system in two ways: - adding parsing and pretty-printing rules (chapter - \ref{Addoc-syntax}) and writing new tactics (chapter - \ref{TacticLanguage}) + adding parsing and pretty-printing rules + (Chapter~\ref{Addoc-syntax}) and writing new tactics + (Chapter~\ref{TacticLanguage}). \item In the fourth part more practical tools are documented. First in - the chapter \ref{Addoc-coqc} the usage of \texttt{coqc} (batch mode) + Chapter~\ref{Addoc-coqc}, the usage of \texttt{coqc} (batch mode) and \texttt{coqtop} (interactive mode) with their options is - described. Then (in chapter \ref{Utilities}) + described. Then, in Chapter~\ref{Utilities}, various utilities that come with the \Coq\ distribution are presented. - Finally, chapter~\ref{Addoc-coqide} describes the \Coq{} integrated + Finally, Chapter~\ref{Addoc-coqide} describes the \Coq{} integrated development environment. \end{itemize} @@ -97,14 +97,14 @@ a tactic index and a vernacular command index. \section*{List of additional documentation} -This manual contains not all the documentation the user may need about -Coq. Various informations can be found in the following documents: - +This manual does not contain all the documentation the user may need +about \Coq{}. Various informations can be found in the following +documents: \begin{description} \item[Tutorial] - A companion volume to this reference manual, the \Coq\ Tutorial, is - aimed at gently introducing new users to developing proofs in \Coq\ + A companion volume to this reference manual, the \Coq{} Tutorial, is + aimed at gently introducing new users to developing proofs in \Coq{} without assuming prior knowledge of type theory. In a second step, the user can read also the tutorial on recursive types (document {\tt RecTutorial.ps}). @@ -119,11 +119,11 @@ Coq. Various informations can be found in the following documents: to the Addendum. \item[Installation] A text file INSTALL that comes with the sources - explains how to install \Coq. A file UNINSTALL explains how + explains how to install \Coq{}. A file UNINSTALL explains how uninstall or move it. -\item[The \Coq\ standard library] -A commented version of sources of the \Coq\ standard library +\item[The \Coq{} standard library] +A commented version of sources of the \Coq{} standard library (including only the specifications, the proofs are removed) is given in the additional document {\tt Library.ps}. diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex index 15dd54be2..404ca5f78 100755 --- a/doc/RefMan-pre.tex +++ b/doc/RefMan-pre.tex @@ -6,44 +6,44 @@ development of computer programs consistent with their formal specification. It is the result of about ten years of research of the Coq project. We shall briefly survey here three main aspects: the -{\sl logical language} in which we write our axiomatizations and -specifications, the {\sl proof assistant} which allows the development -of verified mathematical proofs, and the {\sl program extractor} which +\emph{logical language} in which we write our axiomatizations and +specifications, the \emph{proof assistant} which allows the development +of verified mathematical proofs, and the \emph{program extractor} which synthesizes 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 the {\sl Calculus of Inductive Constructions}. Without going +called the \emph{Calculus of Inductive Constructions}. Without going back to Leibniz and Boole, we can date the creation of what is now called mathematical logic to the work of Frege and Peano at the turn of the century. The discovery of antinomies in the free use of predicates or comprehension principles prompted Russell to restrict -predicate calculus with a stratification of {\sl types}. This effort -culminated with {\sl Principia Mathematica}, the first systematic +predicate calculus with a stratification of \emph{types}. This effort +culminated with \emph{Principia Mathematica}, the first systematic attempt at a formal foundation of mathematics. A simplification of this system along the lines of simply typed $\lambda$-calculus -occurred with Church's {\sl Simple Theory of Types}. The +occurred with Church's \emph{Simple Theory of Types}. The $\lambda$-calculus notation, originally used for expressing functionality, could also be used as an encoding of natural deduction proofs. This Curry-Howard isomorphism was used by N. de Bruijn in the -{\sl Automath} project, the first full-scale attempt to develop and +\emph{Automath} project, the first full-scale attempt to develop and mechanically verify mathematical proofs. This effort culminated with -Jutting's verification of Landau's {\sl Grundlagen} in the 1970's. +Jutting's verification of Landau's \emph{Grundlagen} in the 1970's. Exploiting this Curry-Howard isomorphism, notable achievements in proof theory saw the emergence of two type-theoretic frameworks; the -first one, Martin-L\"of's {\sl Intuitionistic Theory of Types}, +first one, Martin-L\"of's \emph{Intuitionistic Theory of Types}, attempts a new foundation of mathematics on constructive principles. The second one, Girard's polymorphic $\lambda$-calculus $F_\omega$, is a very strong functional system in which we may represent higher-order logic proof structures. Combining both systems in a higher-order extension of the Automath languages, T. Coquand presented in 1985 the -first version of the {\sl Calculus of Constructions}, CoC. This strong +first version of the \emph{Calculus of Constructions}, CoC. This strong logical system allowed powerful axiomatizations, but direct inductive definitions were not possible, and inductive notions had to be defined indirectly through functional encodings, which introduced inefficiencies and awkwardness. The formalism was extended in 1989 by T. Coquand and C. Paulin with primitive inductive definitions, leading -to the current {\sl Calculus of Inductive Constructions}. This +to the current \emph{Calculus of Inductive Constructions}. This extended formalism is not rigorously defined here. Rather, numerous concrete examples are discussed. We refer the interested reader to relevant research papers for more information about the formalism, its @@ -58,8 +58,8 @@ Automated theorem-proving was pioneered in the 1960's by Davis and Putnam in propositional calculus. A complete mechanization (in the sense of a semi-decision procedure) of classical first-order logic was proposed in 1965 by J.A. Robinson, with a single uniform inference -rule called {\sl resolution}. Resolution relies on solving equations -in free algebras (i.e. term structures), using the {\sl unification +rule called \emph{resolution}. Resolution relies on solving equations +in free algebras (i.e. term structures), using the \emph{unification algorithm}. Many refinements of resolution were studied in the 1970's, but few convincing implementations were realized, except of course that PROLOG is in some sense issued from this effort. A less @@ -71,7 +71,7 @@ semantics recursion equations, and the Boyer and Moore theorem-prover, an automation of primitive recursion over inductive data types. While the Boyer-Moore theorem-prover attempted to synthesize proofs by a combination of automated methods, LCF constructed its proofs through -the programming of {\sl tactics}, written in a high-level functional +the programming of \emph{tactics}, written in a high-level functional meta-language, ML. The salient feature which clearly distinguishes our proof assistant @@ -93,7 +93,7 @@ research in artificial intelligence, pioneered by R. Waldinger. The Tablog system of Z. Manna and R. Waldinger allows the deductive synthesis of functional programs from proofs in tableau form of their specifications, written in a variety of first-order logic. Development -of a systematic {\sl programming logic}, based on extensions of +of a systematic \emph{programming logic}, based on extensions of Martin-L\"of's type theory, was undertaken at Cornell U. by the Nuprl team, headed by R. Constable. The first actual program extractor, PX, was designed and implemented around 1985 by S. Hayashi from Kyoto @@ -113,18 +113,18 @@ A first implementation of CoC was started in 1984 by G. Huet and T. Coquand. Its implementation language was CAML, a functional programming language from the ML family designed at INRIA in Rocquencourt. The core of this system was a proof-checker for CoC seen -as a typed $\lambda$-calculus, called the {\sl Constructive Engine}. +as a typed $\lambda$-calculus, called the \emph{Constructive Engine}. This engine was operated through a high-level notation permitting the declaration of axioms and parameters, the definition of mathematical types and objects, and the explicit construction of proof objects encoded as $\lambda$-terms. A section mechanism, designed and implemented by G. Dowek, allowed hierarchical developments of -mathematical theories. This high-level language was called the {\sl - Mathematical Vernacular}. Furthermore, an interactive {\sl Theorem - Prover} permitted the incremental construction of proof trees in a -top-down manner, subgoaling recursively and backtracking from -dead-alleys. The theorem prover executed tactics written in CAML, in -the LCF fashion. A basic set of tactics was predefined, which the +mathematical theories. This high-level language was called the +\emph{Mathematical Vernacular}. Furthermore, an interactive +\emph{Theorem Prover} permitted the incremental construction of proof +trees in a top-down manner, subgoaling recursively and backtracking +from dead-alleys. The theorem prover executed tactics written in CAML, +in the LCF fashion. A basic set of tactics was predefined, which the user could extend by his own specific tactics. This system (Version 4.10) was released in 1989. Then, the system was extended to deal with the new calculus with inductive types by C. Paulin, with @@ -138,21 +138,21 @@ implemented by A. Felty. It allowed operation of the theorem-prover through the manipulation of windows, menus, mouse-sensitive buttons, and other widgets. 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 -Coq was then coordinated by C. Murthy, with new tools designed by C. -Parent to prove properties of ML programs (this methodology is dual to -program extraction) and a new user-interaction loop. This system -(Version 5.8) was released in May 1993. A Centaur interface CTCoq was -then developed by Y. Bertot from the Croap project from -INRIA-Sophia-Antipolis. +\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 \Coq{} was then coordinated by C. Murthy, with new tools designed +by C. Parent to prove properties of ML programs (this methodology is +dual to program extraction) and a new user-interaction loop. This +system (Version 5.8) was released in May 1993. A Centaur interface +\textsc{CTCoq} was then developed by 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 -consistently with dependent types in an experimental version of Coq +consistently with dependent types in an experimental version of \Coq{} (V5.9). -The version V5.10 of Coq is based on a generic system for +The version V5.10 of \Coq{} is based on a generic system for manipulating terms with binding operators due to Chet Murthy. A new proof engine allows the parallel development of partial proofs for independent subgoals. The structure of these proof trees is a mixed @@ -198,14 +198,14 @@ Gérard Huet \section*{Credits: addendum for version 6.1} %\addcontentsline{toc}{section}{Credits: addendum for version V6.1} -The present version 6.1 of Coq is based on the V5.10 architecture. It +The present version 6.1 of \Coq{} is based on the V5.10 architecture. It was ported to the new language Objective Caml by Bruno Barras. The underlying framework has slightly changed and allows more conversions between sorts. The new version provides powerful tools for easier developments. -Cristina Cornes designed an extension of the Coq syntax to allow +Cristina Cornes designed an extension of the \Coq{} syntax to allow definition of terms using a powerful pattern-matching analysis in the style of ML programs. @@ -218,14 +218,14 @@ do not need to be explicitly written. Yann Coscoy designed a command which explains a proof term using natural language. Pierre Cr{\'e}gut built a new tactic which solves problems in quantifier-free Presburger Arithmetic. Both -functionalities have been integrated to the Coq system by Hugo +functionalities have been integrated to the \Coq{} system by Hugo Herbelin. Samuel Boutin designed a tactic for simplification of commutative rings using a canonical set of rewriting rules and equality modulo associativity and commutativity. -Finally the organisation of the \Coq\ distribution has been supervised +Finally the organisation of the \Coq{} distribution has been supervised by Jean-Christophe Filliâtre with the help of Judicaël Courant and Bruno Barras. @@ -237,11 +237,11 @@ Christine Paulin \section*{Credits: addendum for version 6.2} %\addcontentsline{toc}{section}{Credits: addendum for version V6.2} -In version 6.2 of Coq, the parsing is done using camlp4, a +In version 6.2 of \Coq{}, the parsing is done using camlp4, a preprocessor and pretty-printer for CAML designed by Daniel de Rauglaudre at INRIA. Daniel de Rauglaudre made the first adaptation -of Coq for camlp4, this work was continued by Bruno Barras who also -changed the structure of Coq abstract syntax trees and the primitives +of \Coq{} for camlp4, this work was continued by Bruno Barras who also +changed the structure of \Coq{} abstract syntax trees and the primitives to manipulate them. The result of these changes is a faster parsing procedure with greatly improved syntax-error messages. The user-interface to introduce grammar or @@ -249,32 +249,30 @@ pretty-printing rules has also changed. Eduardo Giménez redesigned the internal tactic libraries, giving uniform names -to Caml functions corresponding to Coq tactic names. +to Caml functions corresponding to \Coq{} tactic names. Bruno Barras wrote new more efficient reductions functions. -Hugo Herbelin introduced more uniform notations in the Coq -specification language : the -definitions by fixpoints and pattern-matching have a more readable -syntax. -Patrick Loiseleur introduced user-friendly notations for arithmetic -expressions. +Hugo Herbelin introduced more uniform notations in the \Coq{} +specification language: the definitions by fixpoints and +pattern-matching have a more readable syntax. Patrick Loiseleur +introduced user-friendly notations for arithmetic expressions. New tactics were introduced: Eduardo Giménez improved a mechanism to introduce macros for tactics, and designed special tactics for (co)inductive definitions; Patrick Loiseleur designed a tactic to simplify polynomial expressions in an arbitrary commutative ring which generalizes the previous tactic implemented by Samuel Boutin. -Jean-Christophe Filli\^atre introduced a tactic for refining a goal, +Jean-Christophe Filli\^atre introduced a tactic for refining a goal, using a proof term with holes as a proof scheme. David Delahaye designed the \textsf{SearchIsos} tool to search an object in the library given its type (up to isomorphism). -Henri Laulhère produced the Coq distribution for the Windows environment. +Henri Laulhère produced the \Coq{} distribution for the Windows environment. -Finally, Hugo Herbelin was the main coordinator of the Coq documentation with -principal contributions by Bruno Barras, David Delahaye, +Finally, Hugo Herbelin was the main coordinator of the \Coq{} +documentation with principal contributions by Bruno Barras, David Delahaye, Jean-Christophe Filli\^atre, Eduardo Giménez, Hugo Herbelin and Patrick Loiseleur. diff --git a/doc/macros.tex b/doc/macros.tex index 69488bfb3..080aeb77a 100755 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -67,6 +67,7 @@ \newcommand{\Gallina}{\textsc{Gallina}} \newcommand{\coqide}{\textsc{CoqIDE}} \newcommand{\CoqIde}{\textsc{CoqIDE}} +\newcommand{\CoqIDE}{\textsc{CoqIDE}} \newcommand{\ocaml}{\textsc{Objective Caml}} \newcommand{\camlpppp}{\textsc{Camlp4}} \newcommand{\emacs}{\textsc{GNU Emacs}} @@ -366,7 +367,7 @@ \newcommand{\irule}[3]{{\irulehelp{#1}{#2}{#3} \hbox to \wd\tempa{\hss \box\tempb \hss}}} -\newcommand{\sverb}[1]{\tt #1} +\newcommand{\sverb}[1]{{\tt #1}} \newcommand{\mover}[2]{{#1\over #2}} \newcommand{\jd}[2]{#1 \vdash #2} \newcommand{\mathline}[1]{\[#1\]} |