diff options
Diffstat (limited to 'doc/refman/RefMan-lib.tex')
| -rw-r--r-- | doc/refman/RefMan-lib.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index f1913d7cc4..33c68e49d7 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -12,12 +12,12 @@ The \Coq\ library is structured into three parts: various developments of \Coq\ axiomatizations about sets, lists, sorting, arithmetic, etc. This library comes with the system and its modules are directly accessible through the \verb!Require! command - (see section~\ref{Require}); + (see Section~\ref{Require}); \item[User contributions:] Other specification and proof developments coming from the \Coq\ users' community. These libraries are available for download at \texttt{http://coq.inria.fr} (see - section~\ref{Contributions}). + Section~\ref{Contributions}). \end{description} This chapter briefly reviews these libraries. @@ -112,7 +112,7 @@ The basic library of {\Coq} comes with the definitions of standard (intuitionistic) logical connectives (they are defined as inductive constructions). They are equipped with an appealing syntax enriching the (subclass {\form}) of the syntactic class {\term}. The syntax -extension is shown on figure \ref{formulas-syntax}. +extension is shown on Figure~\ref{formulas-syntax}. % The basic library of {\Coq} comes with the definitions of standard % (intuitionistic) logical connectives (they are defined as inductive @@ -819,7 +819,7 @@ subdirectories: These directories belong to the initial load path of the system, and the modules they provide are compiled at installation time. So they are directly accessible with the command \verb!Require! (see -chapter~\ref{Other-commands}). +Chapter~\ref{Other-commands}). The different modules of the \Coq\ standard library are described in the additional document \verb!Library.dvi!. They are also accessible on the WWW @@ -828,7 +828,7 @@ through the \Coq\ homepage \subsection[Notations for integer arithmetics]{Notations for integer arithmetics\index{Arithmetical notations}} -On figure \ref{zarith-syntax} is described the syntax of expressions +On Figure~\ref{zarith-syntax} is described the syntax of expressions for integer arithmetics. It is provided by requiring and opening the module {\tt ZArith} and opening scope {\tt Z\_scope}. |