diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/.cvsignore | 2 | ||||
| -rw-r--r-- | doc/Correctness.tex (renamed from doc/Programs.tex) | 3 | ||||
| -rwxr-xr-x | doc/Library.tex | 30 | ||||
| -rw-r--r-- | doc/Reference-Manual.tex | 2 |
4 files changed, 21 insertions, 16 deletions
diff --git a/doc/.cvsignore b/doc/.cvsignore index e451a5f0d..2a42b2655 100644 --- a/doc/.cvsignore +++ b/doc/.cvsignore @@ -28,3 +28,5 @@ config.cache config.status Makefile Reference-Manual.rel +library.files +library.coqweb.tex diff --git a/doc/Programs.tex b/doc/Correctness.tex index 4ff14eb63..1b24207f6 100644 --- a/doc/Programs.tex +++ b/doc/Correctness.tex @@ -19,7 +19,6 @@ it when necessary, with the following command: $$ \mbox{\texttt{Require Correctness.}} $$ -\emph{Be aware that this tactic is still very experimental}. %%%%%%%%%%%%%%%%%%%%% @@ -635,7 +634,7 @@ The first set of libraries is automatically loaded with the module \item[Arrays]: this module defines an abstract type \texttt{array} for arrays, with the corresponding operations \texttt{new}, \texttt{access} and \texttt{store}. Access in a array $t$ at index - $i$ may be written \texttt{$t$\#[$i$]} in \Coq, and in particular + $i$ may be written \texttt{\#$t$[$i$]} in \Coq, and in particular inside specifications. This module also provides some axioms to manipulate arrays expression, among which \texttt{store\_def\_1} and diff --git a/doc/Library.tex b/doc/Library.tex index d9a67061a..321c4057e 100755 --- a/doc/Library.tex +++ b/doc/Library.tex @@ -1,8 +1,12 @@ \documentclass[11pt]{article} +\usepackage[latin1]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage[noweb]{coqweb} + \input{./title} \input{./macros} -\input{./library/macros} \begin{document} @@ -25,21 +29,21 @@ The standard library is composed of the following subdirectories: \medskip \begin{tabular}{lp{12cm}} {\bf Logic} & Classical logic and dependent equality \\ + {\bf Bool} & Booleans (basic functions and results) \\ {\bf Arith} & Basic Peano arithmetic \\ {\bf Zarith} & Basic integer arithmetic \\ - {\bf Bool} & Booleans (basic functions and results) \\ + {\bf Reals} & Axiomatization of Real Numbers (classical, basic functions + and results, integer part and fractional part, + requires the \textbf{Zarith} library).\\ {\bf Lists} & Monomorphic and polymorphic lists (basic functions and - results), Streams (infinite sequences defined with co-inductive - types) \\ + results), Streams (infinite sequences defined + with co-inductive types) \\ {\bf Sets} & Sets (classical, constructive, finite, infinite, power set, - etc.) \\ - {\bf IntMap} & Representation of finite sets by an efficient - structure of map (trees indexed by binary integers).\\ - {\bf Reals} & Axiomatization of Real Numbers (classical, basic functions - and results, integer part and fractional part, - requires the \textbf{Zarith} library).\\ - {\bf Relations} & Relations (definitions and basic results). \\ - {\bf Wellfounded} & Well-founded relations (basic results). \\ + etc.) \\ + {\bf Relations} & Relations (definitions and basic results). \\ + {\bf Wellfounded} & Well-founded relations (basic results). \\ + {\bf IntMap} & Representation of finite sets by an efficient + structure of map (trees indexed by binary integers).\\ \end{tabular} \medskip @@ -51,7 +55,7 @@ is also a version of this document in HTML format on the WWW, which you can access from the \Coq\ home page at \texttt{http://pauillac.inria.fr/coq/coq-eng.html}. -\input{library/libdoc.tex} +\input{library.coqweb.tex} \end{document} diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex index 599fa3fe6..516a3f9d9 100644 --- a/doc/Reference-Manual.tex +++ b/doc/Reference-Manual.tex @@ -54,7 +54,7 @@ %%SUPPRIME \include{Natural.v}% \include{Omega.v}% %%SUPPRIME \include{Program.v}% -\include{Programs.v}% = preuve de pgms imperatifs +\include{Correctness.v}% = preuve de pgms imperatifs \include{Extraction.v}% \include{Polynom.v}% = Ring |