diff options
Diffstat (limited to 'doc/refman/RefMan-tus.tex')
| -rw-r--r-- | doc/refman/RefMan-tus.tex | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex index 9b3745a0b..d7239c8fd 100644 --- a/doc/refman/RefMan-tus.tex +++ b/doc/refman/RefMan-tus.tex @@ -665,7 +665,7 @@ constructor patterns, wild-cards, etc, into terms that only use the primitive \textsl{Case} described in Chapter \ref{Cic} \item Restoring type coercions and synthesizing the implicit arguments (the one denoted by question marks in -{\Coq} syntax: cf section \ref{Coercions}). +{\Coq} syntax: see Section~\ref{Coercions}). \item Transforming the named bound variables into deBrujin's indexes. \item Classifying the global names into the different classes of constants (defined constants, constructors, inductive types, etc). @@ -708,7 +708,7 @@ completed, and a construction can be generated from the proof tree, replacing each of the existential variables by its definition. This is exactly what happens when one of the commands \texttt{Qed}, \texttt{Save} or \texttt{Defined} is invoked -(cf. Section \ref{Qed}). The saved theorem becomes a defined constant, +(see Section~\ref{Qed}). The saved theorem becomes a defined constant, whose body is the proof object generated. \paragraph{Important:} Before being added to the @@ -766,7 +766,7 @@ arguments for tactics is a union type including: \item well-typed terms, represented by a construction; \item a substitution for bound variables, like the substitution in the tactic \\$\texttt{Apply}\;t\;\texttt{with}\;x:=t_1\ldots -x_n:=t_n$, (cf. Section~\ref{apply}); +x_n:=t_n$, (see Section~\ref{apply}); \item a reduction expression, denoting the reduction strategy to be followed. \end{itemize} @@ -1013,13 +1013,13 @@ the different kinds of errors used in \Coq{} : \fun{val Std.error : string -> 'a} {For simple error messages} \fun{val Std.errorlabstrm : string -> std\_ppcmds -> 'a} - {See section \ref{PrettyPrinter} : this can be used if the user + {See Section~\ref{PrettyPrinter} : this can be used if the user want to display a term or build a complex error message} \fun{exception Anomaly of string * std\_ppcmds} {This for reporting bugs or things that should not happen. The tacticals \texttt{tclTRY} and - \texttt{tclTRY} described in section \ref{OcamlTacticals} catch the + \texttt{tclTRY} described in Section~\ref{OcamlTacticals} catch the exceptions of type \texttt{UserError}, but they don't catch the anomalies. So, in your code, don't raise any anomaly, unless you know what you are doing. We also recommend to avoid constructs @@ -1358,7 +1358,7 @@ its associated grammar rules and the commands to generate a module that can be loaded dynamically from \Coq's toplevel. To compile our project, we will create a \texttt{Makefile} with the -command \texttt{do\_Makefile} (see section \ref{Makefile}) : +command \texttt{do\_Makefile} (see Section~\ref{Makefile}) : \begin{quotation} \texttt{do\_Makefile eqdecide.ml EqDecide.v > Makefile}\\ @@ -1489,7 +1489,7 @@ The tactic will depend on the \Coq modules \texttt{Logic} and propositional equality (\texttt{eq}), computational disjunction (\texttt{sumbool}), and logical negation (\texttt{not}), defined in that modules. This is specified creating the module maker -\texttt{mmk} (cf. Section \ref{Patterns}). +\texttt{mmk} (see Section~\ref{Patterns}). The third step of the procedure can be divided into three sub-steps. Assume that both $x$ and $y$ have been introduced by the same @@ -1737,7 +1737,7 @@ is not displayed, since we have chosen to hide its implementation. When your tactic does not behave as expected, it is possible to trace it dynamically from \Coq. In order to do this, you have first to leave the toplevel of \Coq, and come back to the \ocaml{} interpreter. This can -be done using the command \texttt{Drop} (cf. Section \ref{Drop}). Once +be done using the command \texttt{Drop} (see Section~\ref{Drop}). Once in the \ocaml{} toplevel, load the file \texttt{tactics/include.ml}. This file installs several pretty printers for proof trees, goals, terms, abstract syntax trees, names, etc. It also contains the @@ -1791,7 +1791,7 @@ these macros need to be compiled by giving to {\tt ocamlc} the option \verb=-pp "camlp4o -I $(COQTOP)/parsing grammar.cma pa_extend.cmo"= \noindent which is the default for every file compiled by means of a Makefile -generated by {\tt coq\_makefile} (cf chapter \ref {Addoc-coqc}). So, +generated by {\tt coq\_makefile} (see Chapter~\ref{Addoc-coqc}). So, just do \verb=make= in this latter case. The syntax of the macros is given on figure @@ -1906,7 +1906,7 @@ In case parsing the arguments of the tactic or the vernacular command involves grammar entries other than the predefined entries listed above, you have to declare a new entry using the macros \verb=ARGUMENT EXTEND= or \verb=VERNAC ARGUMENT EXTEND=. The syntax is -given on figure \ref{ARGUMENT-EXTEND-syntax}. Notice that arguments +given on Figure~\ref{ARGUMENT-EXTEND-syntax}. Notice that arguments declared by \verb=ARGUMENT EXTEND= can be used for arguments of both tactics and vernacular commands while arguments declared by \verb=VERNAC ARGUMENT EXTEND= can only be used by vernacular commands. |