From 1fea3d95ea731826c4c0e4b6943c0d421c9d5271 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 5 Jan 2008 14:06:51 +0000 Subject: Standardisation du format des références croisées vers Figure, Section, Chapter Remplacement pageref par ref parce que pageref n'a pas de sens pour la version HTML MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10421 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/refman/Cases.tex | 6 ++--- doc/refman/Coercion.tex | 2 +- doc/refman/Extraction.tex | 2 +- doc/refman/Program.tex | 8 +++---- doc/refman/RefMan-cic.tex | 22 +++++++++--------- doc/refman/RefMan-coi.tex | 2 +- doc/refman/RefMan-com.tex | 8 +++---- doc/refman/RefMan-ext.tex | 28 +++++++++++------------ doc/refman/RefMan-gal.tex | 29 +++++++++++------------ doc/refman/RefMan-ind.tex | 2 +- doc/refman/RefMan-int.tex | 2 +- doc/refman/RefMan-lib.tex | 10 ++++---- doc/refman/RefMan-ltac.tex | 6 ++--- doc/refman/RefMan-oth.tex | 46 ++++++++++++++++++------------------- doc/refman/RefMan-pro.tex | 18 +++++++-------- doc/refman/RefMan-syn.tex | 22 +++++++++--------- doc/refman/RefMan-tac.tex | 56 ++++++++++++++++++++++----------------------- doc/refman/RefMan-tacex.tex | 2 +- doc/refman/RefMan-tus.tex | 20 ++++++++-------- doc/refman/RefMan-uti.tex | 8 +++---- 20 files changed, 150 insertions(+), 149 deletions(-) diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex index 345608c6f..a0f483ab0 100644 --- a/doc/refman/Cases.tex +++ b/doc/refman/Cases.tex @@ -11,7 +11,7 @@ This section describes the full form of pattern-matching in {\Coq} terms. \asection{Patterns}\label{implementation} The full syntax of {\tt -match} is presented in figures~\ref{term-syntax} +match} is presented in Figures~\ref{term-syntax} and~\ref{term-syntax-aux}. Identifiers in patterns are either constructor names or variables. Any identifier that is not the constructor of an inductive or coinductive type is considered to be a @@ -472,7 +472,7 @@ In all the previous examples the elimination predicate does not depend on the object(s) matched. But it may depend and the typical case is when we write a proof by induction or a function that yields an object of dependent type. An example of proof using \texttt{match} in -given in section \ref{refine-example} +given in Section~\ref{refine-example} For example, we can write the function \texttt{buildlist} that given a natural number @@ -524,7 +524,7 @@ the second is not. % $[\vec{d_1}:\vec{D_1}][x_1:T_1]\ldots [\vec{d_n}:\vec{D_n}][x_n:T_n]Q.$ The user can also use \texttt{match} in combination with the tactic -\texttt{refine} (see section \ref{refine}) to build incomplete proofs +\texttt{refine} (see Section~\ref{refine}) to build incomplete proofs beginning with a \texttt{match} construction. \asection{Pattern-matching on inductive objects involving local diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex index 5445224b0..b4bae4235 100644 --- a/doc/refman/Coercion.tex +++ b/doc/refman/Coercion.tex @@ -327,7 +327,7 @@ By default, a coercion is never printed. \index{Coercions!and records} We allow the definition of {\em Structures with Inheritance} (or classes as records) by extending the existing {\tt Record} macro -(see section~\ref{Record}). Its new syntax is: +(see Section~\ref{Record}). Its new syntax is: \begin{center} \begin{tabular}{l} diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index c8daea1dc..da9b3e717 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -182,7 +182,7 @@ this constant is not declared in the generated file. \asubsection{Realizing axioms}\label{extraction:axioms} Extraction will fail if it encounters an informative -axiom not realized (see section \ref{extraction:axioms}). +axiom not realized (see Section~\ref{extraction:axioms}). A warning will be issued if it encounters an logical axiom, to remind user that inconsistant logical axioms may lead to incorrect or non-terminating extracted terms. diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 6c30e23fc..0d9422dd9 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -14,7 +14,7 @@ We present here the new \Program\ tactic commands, used to build certified \Coq\ programs, elaborating them from their algorithmic skeleton and a rich specification \cite{Sozeau06}. It can be sought of as a dual of extraction -(chapter \ref{Extraction}). The goal of \Program~is to program as in a regular +(see Chapter~\ref{Extraction}). The goal of \Program~is to program as in a regular functional programming language whilst using as rich a specification as desired and proving that the code meets the specification using the whole \Coq{} proof apparatus. This is done using a technique originating from the @@ -44,7 +44,7 @@ generate an obligation for every such coercion. In the other direction, Another distinction is the treatment of pattern-matching. Apart from the following differences, it is equivalent to the standard {\tt match} -operation (section \ref{Caseexpr}). +operation (see Section~\ref{Caseexpr}). \begin{itemize} \item Generation of equalities. A {\tt match} expression is always generalized by the corresponding equality. As an example, @@ -82,7 +82,7 @@ fall back directly to \Coq's usual typing of dependent pattern-matching. The next two commands are similar to their standard counterparts -Definition (section \ref{Simpl-definitions}) and Fixpoint (section \ref{Fixpoint}) in that +Definition (see Section~\ref{Simpl-definitions}) and Fixpoint (see Section~\ref{Fixpoint}) in that they define constants. However, they may require the user to prove some goals to construct the final definitions. @@ -129,7 +129,7 @@ obligations. Once solved using the commands shown below, it binds the final \label{ProgramFixpoint}} The structural fixpoint operator behaves just like the one of Coq -(section \ref{Fixpoint}), except it may also generate obligations. +(see Section~\ref{Fixpoint}), except it may also generate obligations. It works with mutually recursive definitions too. \begin{coq_example} diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 7759b8055..dc7235ae6 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -16,7 +16,7 @@ We call this calculus the {\em Predicative Calculus of (Co)Inductive Constructions}\index{Predicative Calculus of (Co)Inductive Constructions} (\pCIC\ in short). -In section~\ref{impredicativity} we give the extra-rules for \iCIC. A +In Section~\ref{impredicativity} we give the extra-rules for \iCIC. A compiling option of \Coq{} allows to type-check theories in this extended system. @@ -28,7 +28,7 @@ type. For instance, the statement {\it ``for all x, P''} is not allowed in type theory; you must say instead: {\it ``for all x belonging to T, P''}. The expression {\it ``x belonging to T''} is written {\it ``x:T''}. One also says: {\it ``x has type T''}. -The terms of {\CIC} are detailed in section \ref{Terms}. +The terms of {\CIC} are detailed in Section~\ref{Terms}. In \CIC\, there is an internal reduction mechanism. In particular, it allows to decide if two programs are {\em intentionally} equal (one @@ -132,7 +132,7 @@ the universe variables is maintained globally. To ensure the existence of a mapping of the universes to the positive integers, the graph of constraints must remain acyclic. Typing expressions that violate the acyclicity of the graph of constraints results in a \errindex{Universe -inconsistency} error (see also section~\ref{PrintingUniverses}). +inconsistency} error (see also Section~\ref{PrintingUniverses}). \subsection{Constants} Besides the sorts, the language also contains constants denoting @@ -266,7 +266,7 @@ names. Declarations are either assumptions or ``standard'' definitions, that is abbreviations for well-formed terms but also definitions of inductive objects. In the latter case, an object in the environment will define one or more constants -(that is types and constructors, see section \ref{Cic-inductive-definitions}). +(that is types and constructors, see Section~\ref{Cic-inductive-definitions}). An assumption will be represented in the environment as \Assum{\Gamma}{c}{T} which means that $c$ is assumed of some type $T$ @@ -346,7 +346,7 @@ be derived from the following rules. \Rem We may have $\kw{let}~x:=t~\kw{in}~u$ well-typed without having $((\lb~x:T\mto u)~t)$ well-typed (where $T$ is a type of $t$). This is because the value $t$ associated to $x$ -may be used in a conversion rule (see section \ref{conv-rules}). +may be used in a conversion rule (see Section~\ref{conv-rules}). \section[Conversion rules]{Conversion rules\index{Conversion rules} \label{conv-rules}} @@ -372,7 +372,7 @@ refer the interested reader to \cite{Coq85}. \paragraph[$\iota$-reduction.]{$\iota$-reduction.\label{iota}\index{iota-reduction@$\iota$-reduction}} A specific conversion rule is associated to the inductive objects in -the environment. We shall give later on (section \ref{iotared}) the +the environment. We shall give later on (see Section~\ref{iotared}) the precise rules but it just says that a destructor applied to an object built from a constructor behaves as expected. This reduction is called $\iota$-reduction and is more precisely studied in @@ -455,7 +455,7 @@ convertibility rule of \Coq. A term which cannot be any more reduced is said to be in {\em normal form}. There are several ways (or strategies) to apply the reduction rule. Among them, we have to mention the {\em head reduction} which -will play an important role (see chapter \ref{Tactics}). Any term can +will play an important role (see Chapter~\ref{Tactics}). Any term can be written as $\lb~x_1:T_1\mto \ldots \lb x_k:T_k \mto (t_0\ t_1\ldots t_n)$ where $t_0$ is not an application. We say then that $t_0$ is the {\em head @@ -995,7 +995,7 @@ inductive types (i.e. of inductive types with one single constructor and that contains either proofs or inhabitants of singleton types only). More precisely, a small singleton inductive family is set in {\Prop}, a small non singleton inductive family is set in {\Set} (even -in case {\Set} is impredicative -- see section~\ref{impredicativity}), +in case {\Set} is impredicative -- see Section~\ref{impredicativity}), and otherwise in the {\Type} hierarchy. % TODO: clarify the case of a partial application ?? @@ -1529,7 +1529,7 @@ The terms structurally smaller than $y$ are: which one of the $I_l$ occurs) are structurally smaller than $y$. \end{itemize} The following definitions are correct, we enter them using the -{\tt Fixpoint} command as described in section~\ref{Fixpoint} and show +{\tt Fixpoint} command as described in Section~\ref{Fixpoint} and show the internal representation. \begin{coq_example} Fixpoint plus (n m:nat) {struct n} : nat := @@ -1630,14 +1630,14 @@ Abort. \subsubsection{Mutual induction} The principles of mutual induction can be automatically generated -using the {\tt Scheme} command described in section~\ref{Scheme}. +using the {\tt Scheme} command described in Section~\ref{Scheme}. \section{Coinductive types} The implementation contains also coinductive definitions, which are types inhabited by infinite objects. More information on coinductive definitions can be found in~\cite{Gimenez95b,Gim98,GimCas05}. -%They are described in chapter~\ref{Coinductives}. +%They are described in Chapter~\ref{Coinductives}. \section[\iCIC : the Calculus of Inductive Construction with impredicative \Set]{\iCIC : the Calculus of Inductive Construction with diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex index 7de837436..2c0396642 100644 --- a/doc/refman/RefMan-coi.tex +++ b/doc/refman/RefMan-coi.tex @@ -157,7 +157,7 @@ CoFixpoint zeros : Stream nat := cons nat 0%N zeros. CoFixpoint from (n:nat) : Stream nat := cons nat n (from (S n)). \end{coq_example} -As in the \verb!Fixpoint! command (cf. section~\ref{Fixpoint}), it is possible +As in the \verb!Fixpoint! command (see Section~\ref{Fixpoint}), it is possible to introduce a block of mutually dependent methods. The general syntax for this case is : diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index a35f12aa6..845ef7889 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -34,7 +34,7 @@ the Caml toplevel with the command \verb!Drop.!, and come back to the \Coq~toplevel with the command \verb!Toplevel.loop();;!. % The command \verb!coqtop -searchisos! runs the search tool {\sf -% Coq\_SearchIsos} (see section~\ref{coqsearchisos}, +% Coq\_SearchIsos} (see Section~\ref{coqsearchisos}, % page~\pageref{coqsearchisos}) and, as the \Coq~system, can be combined % with the option \verb!-opt!. @@ -44,7 +44,7 @@ looks for a vernacular file named {\em file}{\tt .v}, and tries to compile it into a {\em file}{\tt .vo} file (See ~\ref{compiled}). \Warning The name {\em file} must be a regular {\Coq} identifier, as -defined in the section \ref{lexical}. It +defined in the Section~\ref{lexical}. It must only contain letters, digits or underscores (\_). Thus it can be \verb+/bar/foo/toto.v+ but cannot be \verb+/bar/foo/to-to.v+ . @@ -240,7 +240,7 @@ The following command-line options are recognized by the commands {\tt \item[{\tt -vm}]\ This activates the use of the bytecode-based conversion algorithm - for the current session (see section~\ref{SetVirtualMachine}). + for the current session (see Section~\ref{SetVirtualMachine}). \item[{\tt -image} {\em file}]\ @@ -272,7 +272,7 @@ The following command-line options are recognized by the commands {\tt % \begin{description} % \item[{\tt -searchisos}]\ \\ % Launch the {\sf Coq\_SearchIsos} toplevel -% (see section~\ref{coqsearchisos}, page~\pageref{coqsearchisos}). +% (see Section~\ref{coqsearchisos}, page~\pageref{coqsearchisos}). % \end{description} % $Id$ diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index f6e44f91a..31a1eabb2 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -9,7 +9,7 @@ the Gallina's syntax. The \verb+Record+ construction is a macro allowing the definition of records as is done in many programming languages. Its syntax is -described on figure \ref{record-syntax}. In fact, the \verb+Record+ +described on Figure~\ref{record-syntax}. In fact, the \verb+Record+ macro is more general than the usual record types, since it allows also for ``manifest'' expressions. In this sense, the \verb+Record+ construction allows to define ``signatures''. @@ -231,7 +231,7 @@ construction defined using the extended {\tt match} is generally printed under its expanded form (see~\texttt{Set Printing Matching} in section~\ref{SetPrintingMatching}). -\SeeAlso chapter \ref{Mult-match-full}. +\SeeAlso Chapter~\ref{Mult-match-full}. \subsection{Pattern-matching on boolean values: the {\tt if} expression \label{if-then-else} @@ -283,7 +283,7 @@ Check (fun x (H:{x=0}+{x<>0}) => \end{coq_example} Notice that the printing uses the {\tt if} syntax because {\tt sumbool} is -declared as such (see section \ref{printing-options}). +declared as such (see Section~\ref{printing-options}). \subsection{Irrefutable patterns: the destructuring {\tt let} \index{let in@{\tt let ... in}} @@ -521,7 +521,7 @@ Print fst. % Fix} implementing a combinator for primitive recursion equivalent to % the {\tt Match} construction of \Coq\ V5.8. It is provided only for % sake of compatibility with \Coq\ V5.8. It is recommended to avoid it. -% (see section~\ref{Matchexpr}). +% (see Section~\ref{Matchexpr}). % There is also a notation \texttt{Case} that is the % ancestor of \texttt{match}. Again, it is still in the code for @@ -542,7 +542,7 @@ Print fst. %% It forces the first term to be of type the second term. The %% type must be compatible with %% the term. More precisely it must be either a type convertible to -%% the automatically inferred type (see chapter \ref{Cic}) or a type +%% the automatically inferred type (see Chapter~\ref{Cic}) or a type %% coercible to it, (see \ref{Coercions}). When the type of a %% whole expression is forced, it is usually not necessary to give the types of %% the variables involved in the term. @@ -581,9 +581,9 @@ The {\tt Function} construction enjoys also the {\tt with} extension to define mutually recursive definitions. However, this feature does not work for non structural recursive functions. % VRAI?? -See the documentation of {\tt functional induction} (section -\ref{FunInduction}) and {\tt Functional Scheme} (section -\ref{FunScheme} and \ref{FunScheme-examples}) for how to use the +See the documentation of {\tt functional induction} +(see Section~\ref{FunInduction}) and {\tt Functional Scheme} +(see Section~\ref{FunScheme} and \ref{FunScheme-examples}) for how to use the induction principle to easily reason about the function. \noindent {\bf Remark: } To obtain the right principle, it is better @@ -803,7 +803,7 @@ inside section {\tt s1} and outside. \item Most commands, like {\tt Hint}, {\tt Notation}, option management, ... which appear inside a section are cancelled when the section is closed. -% cf section \ref{LongNames} +% see Section~\ref{LongNames} %\item Usually all identifiers must be distinct. %However, a name already used in a closed section (see \ref{Section}) %can be reused. In this case, the old name is no longer accessible. @@ -1234,7 +1234,7 @@ Conversely, to restore the hidding of implicit arguments, use command {\tt Unset Printing Implicit.} \end{quote} -\SeeAlso {\tt Set Printing All} in section \ref{SetPrintingAll}. +\SeeAlso {\tt Set Printing All} in Section~\ref{SetPrintingAll}. \subsection{Interaction with subtyping} @@ -1377,14 +1377,14 @@ which declares the construction denoted by {\qualid} as a coercion between {\class$_1$} and {\class$_2$}. More details and examples, and a description of the commands related -to coercions are provided in chapter \ref{Coercions-full}. +to coercions are provided in Chapter~\ref{Coercions-full}. \section[Printing constructions in full]{Printing constructions in full\label{SetPrintingAll} \comindex{Set Printing All} \comindex{Unset Printing All}} Coercions, implicit arguments, the type of pattern-matching, but also -notations (see chapter \ref{Addoc-syntax}) can obfuscate the behavior +notations (see Chapter~\ref{Addoc-syntax}) can obfuscate the behavior of some tactics (typically the tactics applying to occurrences of subterms are sensitive to the implicit arguments). The command \begin{quote} @@ -1411,7 +1411,7 @@ The following command: {\tt Set Printing Universes} \end{quote} activates the display of the actual level of each occurrence of -{\Type}. See section~\ref{Sorts} for details. This wizard option, in +{\Type}. See Section~\ref{Sorts} for details. This wizard option, in combination with \texttt{Set Printing All} (see section~\ref{SetPrintingAll}) can help to diagnose failures to unify terms apparently identical but internally different in the Calculus of @@ -1424,7 +1424,7 @@ of the occurrences of {\Type}, use \comindex{Print Universes} The constraints on the internal level of the occurrences of {\Type} -(see section~\ref{Sorts}) can be printed using the command +(see Section~\ref{Sorts}) can be printed using the command \begin{quote} {\tt Print Universes.} \end{quote} diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 8ee30b8fb..23c19d60b 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -1,21 +1,22 @@ \chapter{The \gallina{} specification language \label{Gallina}\index{Gallina}} +\label{BNF-syntax} % Used referred to as a chapter label This chapter describes \gallina, the specification language of {\Coq}. It allows to develop mathematical theories and to prove specifications of programs. The theories are built from axioms, hypotheses, parameters, lemmas, theorems and definitions of constants, functions, predicates and sets. The syntax of logical objects involved in -theories is described in section \ref{term}. The language of +theories is described in Section~\ref{term}. The language of commands, called {\em The Vernacular} is described in section \ref{Vernacular}. In {\Coq}, logical objects are typed to ensure their logical correctness. The rules implemented by the typing algorithm are described in -chapter \ref{Cic}. +Chapter \ref{Cic}. \subsection*{About the grammars in the manual -\label{BNF-syntax}\index{BNF metasyntax}} +\index{BNF metasyntax}} Grammars are presented in Backus-Naur form (BNF). Terminal symbols are set in {\tt typewriter font}. In addition, there are special @@ -219,9 +220,9 @@ possible one (among all tokens defined at this moment), and so on. Figures \ref{term-syntax} and \ref{term-syntax-aux} describe the basic set of terms which form the {\em Calculus of Inductive Constructions} (also called \CIC). The formal presentation of {\CIC} is given in -chapter \ref{Cic}. Extensions of this syntax are given in chapter +Chapter \ref{Cic}. Extensions of this syntax are given in chapter \ref{Gallina-extension}. How to customize the syntax is described in -chapter \ref{Addoc-syntax}. +Chapter \ref{Addoc-syntax}. \begin{figure}[htbp] \begin{centerframe} @@ -363,7 +364,7 @@ denote local {\em variables}, what qualified identifiers do not. Numerals have no definite semantics in the calculus. They are mere notations that can be bound to objects through the notation mechanism -(see chapter~\ref{Addoc-syntax} for details). Initially, numerals are +(see Chapter~\ref{Addoc-syntax} for details). Initially, numerals are bound to Peano's representation of natural numbers (see~\ref{libnats}). @@ -393,7 +394,7 @@ subclass of the syntactic class {\term}. \index{specif@{\specif}} \item {\Type} is the type of {\Set} and {\Prop} \end{itemize} -\noindent More on sorts can be found in section \ref{Sorts}. +\noindent More on sorts can be found in Section~\ref{Sorts}. \bigskip @@ -596,10 +597,10 @@ Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) \end{coq_example*} The second subcase is only relevant for annotated inductive types such -as the equality predicate (see section~\ref{Equality}), the order -predicate on natural numbers % (see section~\ref{le}) % undefined reference +as the equality predicate (see Section~\ref{Equality}), the order +predicate on natural numbers % (see Section~\ref{le}) % undefined reference or the type of -lists of a given length (see section~\ref{listn}). In this configuration, +lists of a given length (see Section~\ref{listn}). In this configuration, the type of each branch can depend on the type dependencies specific to the branch and the whole pattern-matching expression has a type determined by the specific dependencies in the type of the term being @@ -1271,7 +1272,7 @@ CoInductive Stream : Set := \end{coq_example} The syntax of this command is the same as the command \texttt{Inductive} -(cf. Section~\ref{gal_Inductive_Definitions}). Notice that no +(see Section~\ref{gal_Inductive_Definitions}). Notice that no principle of induction is derived from the definition of a co-inductive type, since such principles only make sense for inductive ones. For co-inductive ones, the only elimination principle is case @@ -1525,7 +1526,7 @@ Eval compute in (tl (from 0)). with\\ \mbox{}\hspace{0.1cm} $\ldots$ \\ with {\ident$_m$} : {\type$_m$} := {\term$_m$}}\\ -As in the \texttt{Fixpoint} command (cf. Section~\ref{Fixpoint}), it +As in the \texttt{Fixpoint} command (see Section~\ref{Fixpoint}), it is possible to introduce a block of mutually dependent methods. \end{Variants} @@ -1536,7 +1537,7 @@ is possible to introduce a block of mutually dependent methods. A statement claims a goal of which the proof is then interactively done using tactics. More on the proof editing mode, statements and proofs can be -found in chapter \ref{Proof-handling}. +found in Chapter~\ref{Proof-handling}. \subsubsection{\tt Theorem {\ident} : {\type}. \comindex{Theorem} @@ -1586,7 +1587,7 @@ A proof starts by the keyword {\tt Proof}. Then {\Coq} enters the proof editing mode until the proof is completed. The proof editing mode essentially contains tactics that are described in chapter \ref{Tactics}. Besides tactics, there are commands to manage the proof -editing mode. They are described in chapter \ref{Proof-handling}. When +editing mode. They are described in Chapter~\ref{Proof-handling}. When the proof is completed it should be validated and put in the environment using the keyword {\tt Qed}. \medskip diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex index ecb872b0e..23006b72e 100644 --- a/doc/refman/RefMan-ind.tex +++ b/doc/refman/RefMan-ind.tex @@ -18,7 +18,7 @@ macro-generate complicated uses of the basic elimination tactics for inductive types. Sections \ref{inversion_introduction} to \ref{inversion_using} present -inversion tactics and section \ref{scheme} describes +inversion tactics and Section~\ref{scheme} describes a command {\tt Scheme} for automatic generation of induction schemes for mutual inductive types. diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex index c93d7217f..14b14ae57 100644 --- a/doc/refman/RefMan-int.tex +++ b/doc/refman/RefMan-int.tex @@ -48,7 +48,7 @@ commands are processed from a file. the {\tt coqc} command from the operating system. \end{itemize} -These two modes are documented in chapter \ref{Addoc-coqc}. +These two modes are documented in Chapter~\ref{Addoc-coqc}. Other modes of interaction with \Coq{} are possible: through an emacs shell window, an emacs generic user-interface for proof assistant diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index f1913d7cc..33c68e49d 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}. diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 467a47346..48d27a50a 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -27,14 +27,14 @@ problems. \def\cpattern{\nterm{cpattern}} The syntax of the tactic language is given Figures~\ref{ltac} -and~\ref{ltac_aux}. See page~\pageref{BNF-syntax} for a description of +and~\ref{ltac_aux}. See Chapter~\ref{BNF-syntax} for a description of the BNF metasyntax used in these grammar rules. Various already defined entries will be used in this chapter: entries {\naturalnumber}, {\integer}, {\ident}, {\qualid}, {\term}, {\cpattern} and {\atomictac} represent respectively the natural and integer numbers, the authorized identificators and qualified names, {\Coq}'s terms and patterns and all the atomic tactics described in -chapter~\ref{Tactics}. The syntax of {\cpattern} is the same as that +Chapter~\ref{Tactics}. The syntax of {\cpattern} is the same as that of terms, but it is extended with pattern matching metavariables. In {\cpattern}, a pattern-matching metavariable is represented with the syntax {\tt ?id} where {\tt id} is a {\ident}. The notation {\tt \_} @@ -536,7 +536,7 @@ If the evaluation of the right-hand-side of a valid match fails, the next matching subterm is tried. If no further subterm matches, the next clause is tried. Matching subterms are considered top-bottom and from left to right (with respect to the raw printing obtained by -setting option {\tt Printing All}, see section~\ref{SetPrintingAll}). +setting option {\tt Printing All}, see Section~\ref{SetPrintingAll}). \begin{coq_example} Ltac f x := diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 4df212f9e..63e43dd7d 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -64,14 +64,14 @@ the resulting term with its type. The term to be reduced may depend on hypothesis introduced in the first subgoal (if a proof is in progress). -\SeeAlso section~\ref{Conversion-tactics}. +\SeeAlso Section~\ref{Conversion-tactics}. \subsection[\tt Extraction \term.]{\tt Extraction \term.\label{ExtractionTerm} \comindex{Extraction}} This command displays the extracted term from {\term}. The extraction is processed according to the distinction between {\Set} and {\Prop}; that is to say, between logical and -computational content (see section \ref{Sorts}). The extracted term is +computational content (see Section~\ref{Sorts}). The extracted term is displayed in Objective Caml syntax, where global identifiers are still displayed as in \Coq\ terms. @@ -81,7 +81,7 @@ displayed as in \Coq\ terms. globals {\qualid$_1$} \ldots{} {\qualid$_n$}. \end{Variants} -\SeeAlso chapter~\ref{Extraction}. +\SeeAlso Chapter~\ref{Extraction}. \subsection[\tt Opaque \qualid$_1$ \dots \qualid$_n$.]{\tt Opaque \qualid$_1$ \dots \qualid$_n$.\comindex{Opaque}\label{Opaque}} This command tells not to unfold the the constants {\qualid$_1$} \dots {\qualid$_n$} in tactics using @@ -161,7 +161,7 @@ This restricts the search to constructions not defined in modules \begin{ErrMsgs} \item \errindex{Module/section \module{} not found} -No module \module{} has been required (see section~\ref{Require}). +No module \module{} has been required (see Section~\ref{Require}). \end{ErrMsgs} \end{Variants} @@ -425,7 +425,7 @@ for \Coq's toplevel. This kind of file is called a {\em script} for \subsection[\tt Load {\ident}.]{\tt Load {\ident}.\comindex{Load}\label{Load}} This command loads the file named {\ident}{\tt .v}, searching successively in each of the directories specified in the {\em - loadpath}. (see section \ref{loadpath}) + loadpath}. (see Section~\ref{loadpath}) \begin{Variants} \item {\tt Load {\str}.}\label{Load-str}\\ @@ -439,7 +439,7 @@ successively in each of the directories specified in the {\em \comindex{Load Verbose} Display, while loading, the answers of \Coq\ to each command (including tactics) contained in the loaded file - \SeeAlso section \ref{Begin-Silent} + \SeeAlso Section~\ref{Begin-Silent} \end{Variants} \begin{ErrMsgs} @@ -572,7 +572,7 @@ These different variants can be combined. The command did not find the file {\tt toto.vo}. Either {\tt toto.v} exists but is not compiled or {\tt toto.vo} is in a directory - which is not in your {\tt LoadPath} (see section \ref{loadpath}). + which is not in your {\tt LoadPath} (see Section~\ref{loadpath}). \item \errindex{Bad magic number} @@ -582,7 +582,7 @@ These different variants can be combined. version of \Coq. \end{ErrMsgs} -\SeeAlso chapter \ref{Addoc-coqc} +\SeeAlso Chapter~\ref{Addoc-coqc} \subsection[\tt Print Modules.]{\tt Print Modules.\comindex{Print Modules}} This command shows the currently loaded and currently opened @@ -592,10 +592,10 @@ This command shows the currently loaded and currently opened This commands loads the Objective Caml compiled files {\str$_1$} \dots {\str$_n$} (dynamic link). It is mainly used to load tactics dynamically. -% (see chapter \ref{WritingTactics}). +% (see Chapter~\ref{WritingTactics}). The files are searched into the current Objective Caml loadpath (see the command {\tt -Add ML Path} in the section \ref{loadpath}). Loading of Objective Caml +Add ML Path} in the Section~\ref{loadpath}). Loading of Objective Caml files is only possible under the bytecode version of {\tt coqtop} (i.e. {\tt coqtop} called with options {\tt -byte}, see chapter \ref{Addoc-coqc}). @@ -608,14 +608,14 @@ files is only possible under the bytecode version of {\tt coqtop} \subsection[\tt Print ML Modules.]{\tt Print ML Modules.\comindex{Print ML Modules}} This print the name of all \ocaml{} modules loaded with \texttt{Declare ML Module}. To know from where these module were loaded, the user -should use the command \texttt{Locate File} (see page \pageref{Locate File}) +should use the command \texttt{Locate File} (see Section~\ref{Locate File}) \section[Loadpath]{Loadpath\label{loadpath}\index{Loadpath}} There are currently two loadpaths in \Coq. A loadpath where seeking {\Coq} files (extensions {\tt .v} or {\tt .vo} or {\tt .vi}) and one where seeking Objective Caml files. The default loadpath contains the -directory ``\texttt{.}'' denoting the current directory and mapped to the empty logical path (see section \ref{LongNames}). +directory ``\texttt{.}'' denoting the current directory and mapped to the empty logical path (see Section~\ref{LongNames}). \subsection[\tt Pwd.]{\tt Pwd.\comindex{Pwd}\label{Pwd}} This command displays the current working directory. @@ -662,14 +662,14 @@ This command displays the current \Coq\ loadpath. \subsection[\tt Add ML Path {\str}.]{\tt Add ML Path {\str}.\comindex{Add ML Path}} This command adds the path {\str} to the current Objective Caml loadpath (see -the command {\tt Declare ML Module} in the section \ref{compiled}). +the command {\tt Declare ML Module} in the Section~\ref{compiled}). \Rem This command is implied by {\tt Add LoadPath {\str} as {\dirpath}}. \subsection[\tt Add Rec ML Path {\str}.]{\tt Add Rec ML Path {\str}.\comindex{Add Rec ML Path}} This command adds the directory {\str} and all its subdirectories to the current Objective Caml loadpath (see -the command {\tt Declare ML Module} in the section \ref{compiled}). +the command {\tt Declare ML Module} in the Section~\ref{compiled}). \Rem This command is implied by {\tt Add Rec LoadPath {\str} as {\dirpath}}. @@ -727,15 +727,15 @@ This command is dedicated for the use in graphical interfaces. It allows to backtrack to a particular \emph{global} state, i.e. typically a state corresponding to a previous line in a script. A global state includes declaration environment but also proof -environment (see chapter~\ref{Proof-handling}). The three numbers +environment (see Chapter~\ref{Proof-handling}). The three numbers $\num_1$, $\num_2$ and $\num_3$ represent the following: \begin{itemize} \item $\num_3$: Number of \texttt{Abort} to perform, i.e. the number of currently opened nested proofs that must be cancelled (see - chapter~\ref{Proof-handling}). + Chapter~\ref{Proof-handling}). \item $\num_2$: \emph{Proof state number} to unbury once aborts have been done. Coq will compute the number of \texttt{Undo} to perform - (see chapter~\ref{Proof-handling}). + (see Chapter~\ref{Proof-handling}). \item $\num_1$: Environment state number to unbury, Coq will compute the number of \texttt{Back} to perform. \end{itemize} @@ -758,7 +758,7 @@ Where: \begin{itemize} \item \emph{$id_i$} is the name of the current proof (if there is one, otherwise \texttt{Coq} is displayed, see -chapter~\ref{Proof-handling}). +Chapter~\ref{Proof-handling}). \item $\num_1$ is the environment state number after the last command. \item $\num_2$ is the proof state number after the last @@ -814,7 +814,7 @@ use in a further session. This file can be given as the {\tt \begin{Variants} \item {\tt Write State \ident}\\ Equivalent to {\tt Write State "}{\ident}{\tt .coq"}. - The state is saved in the current directory (see \pageref{Pwd}). + The state is saved in the current directory (see Section~\ref{Pwd}). \end{Variants} \section{Quitting and debugging} @@ -840,7 +840,7 @@ all abstract types of \Coq - section\_path, identfifiers, terms, judgements, \dots. You can also use the file \texttt{base\_include} instead, that loads only the pretty-printers for section\_paths and identifiers. -% See section \ref{test-and-debug} more information on the +% See Section~\ref{test-and-debug} more information on the % usage of the toplevel. You can return back to \Coq{} with the command: @@ -851,9 +851,9 @@ go();; \end{flushleft} \begin{Warnings} -\item It only works with the bytecode version of {\Coq} (i.e. {\tt coqtop} called with option {\tt -byte}, see page \pageref{binary-images}). +\item It only works with the bytecode version of {\Coq} (i.e. {\tt coqtop} called with option {\tt -byte}, see the contents of Section~\ref{binary-images}). \item You must have compiled {\Coq} from the source package and set the - environment variable \texttt{COQTOP} to the root of your copy of the sources (see section \ref{EnvVariables}). + environment variable \texttt{COQTOP} to the root of your copy of the sources (see Section~\ref{EnvVariables}). \end{Warnings} \subsection[\tt Time \textrm{\textsl{command}}.]{\tt Time \textrm{\textsl{command}}.\comindex{Time} @@ -907,7 +907,7 @@ This command displays the current nesting depth used for display. \section{Controlling the conversion algorithm} {\Coq} comes with two algorithms to check the convertibility of types -(see section~\ref{convertibility}). The first algorithm lazily +(see Section~\ref{convertibility}). The first algorithm lazily compares applicative terms while the other is a brute-force but efficient algorithm that first normalizes the terms before comparing them. The second algorithm is based on a bytecode representation of terms diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 1a004b665..d0ca09747 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -2,12 +2,12 @@ \label{Proof-handling}} In \Coq's proof editing mode all top-level commands documented in -chapter \ref{Vernacular-commands} remain available +Chapter~\ref{Vernacular-commands} remain available and the user has access to specialized commands dealing with proof development pragmas documented in this section. He can also use some other specialized commands called {\em tactics}. They are the very tools allowing the user to deal with logical reasoning. They are -documented in chapter \ref{Tactics}.\\ +documented in Chapter~\ref{Tactics}.\\ When switching in editing proof mode, the prompt \index{Prompt} {\tt Coq <} is changed into {\tt {\ident} <} where {\ident} is the @@ -21,7 +21,7 @@ generated by the tactics. To each subgoal is associated a number of hypotheses we call the {\em \index*{local context}} of the goal. Initially, the local context is empty. It is enriched by the use of -certain tactics (see mainly section~\ref{intro}). +certain tactics (see mainly Section~\ref{intro}). When a proof is achieved the message {\tt Proof completed} is displayed. One can then store this proof as a defined constant in the @@ -54,7 +54,7 @@ that goal. %the command {\tt Goal} cannot be used while a proof is already being edited. \end{ErrMsgs} -\SeeAlso section \ref{Theorem} +\SeeAlso Section~\ref{Theorem} \subsection[\tt Qed.]{\tt Qed.\comindex{Qed}\label{Qed}} This command is available in interactive editing proof mode when the @@ -117,7 +117,7 @@ This command switches to interactive editing proof mode and declares as a {\tt Theorem}, the name {\ident} is known at all section levels: {\tt Theorem} is a {\sl global} lemma. -%\ErrMsg (see section \ref{Goal}) +%\ErrMsg (see Section~\ref{Goal}) \begin{ErrMsgs} @@ -164,7 +164,7 @@ as a {\tt Theorem}, the name {\ident} is known at all section levels: \label{BeginProof}} This command applies in proof editing mode. It is equivalent to {\tt exact {\term}; Save.} That is, you have to give the full proof in -one gulp, as a proof term (see section \ref{exact}). +one gulp, as a proof term (see Section~\ref{exact}). \variant {\tt Proof.} @@ -173,7 +173,7 @@ one gulp, as a proof term (see section \ref{exact}). practice to use {\tt Proof.} as an opening parenthesis, closed in the script with a closing {\tt Qed.} -\SeeAlso {\tt Proof with {\tac}.} in section~\ref{ProofWith}. +\SeeAlso {\tt Proof with {\tac}.} in Section~\ref{ProofWith}. \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}} @@ -232,14 +232,14 @@ This commands switches back to the editing of the last edited proof. This command allows to instantiate an existential variable. {\tt \num} is an index in the list of uninstantiated existential variables -displayed by {\tt Show Existentials.} (described in section~\ref{Show}) +displayed by {\tt Show Existentials.} (described in Section~\ref{Show}) This command is intented to be used to instantiate existential variables when the proof is completed but some uninstantiated existential variables remain. To instantiate existential variables during proof edition, you should use the tactic {\tt instantiate}. -\SeeAlso {\tt instantiate (\num:= \term).} in section~\ref{instantiate}. +\SeeAlso {\tt instantiate (\num:= \term).} in Section~\ref{instantiate}. %%%%%%%% diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 9bde8c490..583e4406c 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -7,13 +7,13 @@ commands are {\tt Notation} and {\tt Infix} which are described in section \ref{Notation}. It also happens that the same symbolic notation is expected in different contexts. To achieve this form of overloading, {\Coq} offers a notion of interpretation scope. This is -described in section \ref{scopes}. +described in Section~\ref{scopes}. \Rem The commands {\tt Grammar}, {\tt Syntax} and {\tt Distfix} which were present for a while in {\Coq} are no longer available from {\Coq} version 8.0. The underlying AST structure is also no longer available. The functionalities of the command {\tt Syntactic Definition} are -still available, see section \ref{Abbreviations}. +still available, see Section~\ref{Abbreviations}. \section[Notations]{Notations\label{Notation} \comindex{Notation}} @@ -209,7 +209,7 @@ Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level). For the sake of factorization with {\Coq} predefined rules, simple rules have to be observed for notations starting with a symbol: e.g. rules starting with ``\{'' or ``('' should be put at level 0. The -list of {\Coq} predefined notations can be found in chapter \ref{Theories}. +list of {\Coq} predefined notations can be found in Chapter~\ref{Theories}. The command to display the current state of the {\Coq} term parser is \comindex{Print Grammar constr} @@ -374,7 +374,7 @@ and corecursive definitions can benefit of customized notations. To do this, insert a {\tt where} notation clause after the definition of the (co)inductive type or (co)recursive term (or after the definition of each of them in case of mutual definitions). The exact syntax is given -on Figure \ref{notation-syntax}. Here are examples: +on Figure~\ref{notation-syntax}. Here are examples: \begin{coq_eval} Set Printing Depth 50. @@ -418,7 +418,7 @@ To reactivate it, use the command \end{quote} The default is to use notations for printing terms wherever possible. -\SeeAlso {\tt Set Printing All} in section \ref{SetPrintingAll}. +\SeeAlso {\tt Set Printing All} in Section~\ref{SetPrintingAll}. \subsection{Locating notations \comindex{Locate} @@ -597,8 +597,8 @@ a single identifier. \paragraph{Syntax of notations} The different syntactic variants of the command \texttt{Notation} are -given on Figure \ref{notation-syntax}. The optional {\tt :{\scope}} is -described in the section \ref{scopes}. +given on Figure~\ref{notation-syntax}. The optional {\tt :{\scope}} is +described in the Section~\ref{scopes}. \Rem No typing of the denoted expression is performed at definition time. Type-checking is done only at the time of use of the notation. @@ -743,7 +743,7 @@ is interpreted in the scope stack extended by the scopes bound (if any) to these arguments. \SeeAlso The command to show the scopes bound to the arguments of a -function is described in section \ref{About}. +function is described in Section~\ref{About}. \subsubsection{Binding types of arguments to an interpretation scope} @@ -759,7 +759,7 @@ interpretation of the notation itself expects arguments of the same type that would trigger the same scope). \comindex{Bind Scope} -More generally, any {\class} (see chapter \ref{Coercions-full}) can be +More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be bound to an interpretation scope. The command to do it is \begin{quote} {\tt Bind Scope} {\scope} \texttt{with} {\class} @@ -782,7 +782,7 @@ Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))). interpretation. See the next section. \SeeAlso The command to show the scopes bound to the arguments of a -function is described in section \ref{About}. +function is described in Section~\ref{About}. \subsection[The {\tt type\_scope} interpretation scope]{The {\tt type\_scope} interpretation scope\index{type\_scope}} @@ -878,7 +878,7 @@ This includes the notation for pairs. It is delimited by key {\tt core}. This includes notation for strings as elements of the type {\tt string}. Special characters and escaping follow {\Coq} conventions -on strings (see page~\pageref{strings}). Especially, there is no +on strings (see Section~\ref{strings}). Especially, there is no convention to visualize non printable characters of a string. The file {\tt String.v} shows an example that contains quotes, a newline and a beep (i.e. the ascii character of code 7). diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 335cc3f15..6276b547b 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -33,7 +33,7 @@ satisfied. If it is not the case, the tactic raises an error message. Tactics are build from atomic tactics and tactic expressions (which extends the folklore notion of tactical) to combine those atomic tactics. This chapter is devoted to atomic tactics. The tactic -language will be described in chapter~\ref{TacticLanguage}. +language will be described in Chapter~\ref{TacticLanguage}. There are, at least, three levels of atomic tactics. The simplest one implements basic rules of the logical framework. The second level is @@ -98,7 +98,7 @@ holes. The holes are noted ``\texttt{\_}''. which type cannot be inferred. Put a cast around it. \end{ErrMsgs} -An example of use is given in section~\ref{refine-example}. +An example of use is given in Section~\ref{refine-example}. \section{Basics \index{Typing rules}} @@ -348,7 +348,7 @@ match the current goal against the conclusion of the type of {\term}. If it succeeds, then the tactic returns as many subgoals as the number of non dependent premises of the type of {\term}. The tactic {\tt apply} relies on first-order pattern-matching with dependent -types. See {\tt pattern} in section \ref{pattern} to transform a +types. See {\tt pattern} in Section~\ref{pattern} to transform a second-order pattern-matching problem into a first-order one. \begin{ErrMsgs} @@ -581,7 +581,7 @@ in the list of subgoals remaining to prove. % \vref$_n$ := \term$_n$} % \tacindex{Specialize \dots\ with} \\ % It is to provide the tactic with some explicit values to instantiate -% premises of {\term} (see section \ref{Binding-list}). +% premises of {\term} (see Section~\ref{Binding-list}). % Some other premises are inferred using type information and % unification. The resulting well-formed % term being {\tt (\term~\term'$_1$\dots\term'$_k$)} @@ -685,7 +685,7 @@ to $T$. \label{change}} This tactic applies to any goal. It implements the rule -``Conv''\index{Typing rules!Conv} given in section~\ref{Conv}. {\tt +``Conv''\index{Typing rules!Conv} given in Section~\ref{Conv}. {\tt change U} replaces the current goal \T\ with \U\ providing that \U\ is well-formed and that \T\ and \U\ are convertible. @@ -739,7 +739,7 @@ product {\tt \ident$_i$:T} (for some type \T); if \vref$_i$ is A bindings list can also be a simple list of terms {\tt \term$_1$ \term$_2$ \dots\term$_n$}. In that case the references to which these terms correspond are determined by the tactic. In case of {\tt - elim} (see section~\ref{elim}) the terms should correspond to + elim} (see Section~\ref{elim}) the terms should correspond to all the dependent products in the type of \term\ while in the case of {\tt apply} only the dependent products which are not bound in the conclusion of the type are given. @@ -943,7 +943,7 @@ product or an applicative term in head normal form or a variable. The term \verb+forall n:nat, (plus (S n) (S n))+ is not reduced by {\tt hnf}. \Rem The $\delta$ rule only applies to transparent constants -(see section~\ref{Opaque} on transparency and opacity). +(see Section~\ref{Opaque} on transparency and opacity). \subsection{\tt simpl \tacindex{simpl}} @@ -1575,7 +1575,7 @@ Qed. \item {\tt decompose record \term}\tacindex{decompose record} This decomposes record types (inductive types with one constructor, like \texttt{and} and \texttt{exists} and those defined with the - \texttt{Record} macro, see p.~\pageref{Record}). + \texttt{Record} macro, see Section~\ref{Record}). \end{Variants} @@ -1586,8 +1586,8 @@ Qed. The \emph{experimental} tactic \texttt{functional induction} performs case analysis and induction following the definition of a function. It makes use of a principle generated by \texttt{Function} -(section~\ref{Function}) or \texttt{Functional Scheme} -(section~\ref{FunScheme}). +(see Section~\ref{Function}) or \texttt{Functional Scheme} +(see Section~\ref{FunScheme}). \begin{coq_eval} Reset Initial. @@ -1613,15 +1613,15 @@ you want to write implicit arguments explicitly. \Rem \texttt{functional induction (f x1 x2 x3)} is actually a wrapper for \texttt{induction x1 x2 x3 (f x1 x2 x3) using \qualid} followed by a cleaning phase, where $\qualid$ is the induction principle -registered for $f$ (by the \texttt{Function} (section~\ref{Function}) -or \texttt{Functional Scheme} (section~\ref{FunScheme}) command) +registered for $f$ (by the \texttt{Function} (see Section~\ref{Function}) +or \texttt{Functional Scheme} (see Section~\ref{FunScheme}) command) corresponding to the sort of the goal. Therefore \texttt{functional induction} may fail if the induction scheme (\texttt{\qualid}) is -not defined. See also section~\ref{Function} for the function terms +not defined. See also Section~\ref{Function} for the function terms accepted by \texttt{Function}. \Rem There is a difference between obtaining an induction scheme for a -function by using \texttt{Function} (section~\ref{Function}) and by +function by using \texttt{Function} (see Section~\ref{Function}) and by using \texttt{Functional Scheme} after a normal definition using \texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for details. @@ -1642,7 +1642,7 @@ details. using \term$_{m+1}$ with {\term$_{n+1}$} \dots {\term$_m$}} Similar to \texttt{Induction} and \texttt{elim} - (section~\ref{Tac-induction}), allows to give explicitly the + (see Section~\ref{Tac-induction}), allows to give explicitly the induction principle and the values of dependent premises of the elimination scheme, including \emph{predicates} for mutual induction when \qualid is mutually recursive. @@ -1652,11 +1652,11 @@ details. {\vref$_m$} := {\term$_n$}} Similar to \texttt{induction} and \texttt{elim} - (section~\ref{Tac-induction}). + (see Section~\ref{Tac-induction}). \item All previous variants can be extended by the usual \texttt{as \intropattern} construction, similarly for example to - \texttt{induction} and \texttt{elim} (section~\ref{Tac-induction}). + \texttt{induction} and \texttt{elim} (see Section~\ref{Tac-induction}). \end{Variants} @@ -1857,7 +1857,7 @@ Lemmas are added to the database using the command The tactic is especially useful for parametric setoids which are not accepted as regular setoids for {\tt rewrite} and {\tt - setoid\_replace} (see chapter \ref{setoid_replace}). + setoid\_replace} (see Chapter~\ref{setoid_replace}). \tacindex{stepr} \comindex{Declare Right Step} @@ -2350,7 +2350,7 @@ the instance with the tactic {\tt inversion}. which performs inversion on hypothesis \ident\ of the form \texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ = \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been -defined using \texttt{Function} (section~\ref{Function}). +defined using \texttt{Function} (see Section~\ref{Function}). \begin{ErrMsgs} \item \errindex{Hypothesis \ident must contain at least one Function} @@ -2590,7 +2590,7 @@ and then uses {\tt auto} which completes the proof. Originally due to C{\'e}sar~Mu{\~n}oz, these tactics ({\tt tauto} and {\tt intuition}) have been completely reengineered by David~Delahaye using mainly the tactic -language (see chapter~\ref{TacticLanguage}). The code is now quite shorter and +language (see Chapter~\ref{TacticLanguage}). The code is now quite shorter and a significant increase in performances has been noticed. The general behavior with respect to dependent types, unfolding and introductions has slightly changed to get clearer semantics. This may lead to some @@ -2742,7 +2742,7 @@ vernacular command. % \item {\tt Linear with \ident$_1$ \dots\ \ident$_n$}\\ % \tacindex{Linear with} % Is equivalent to apply first {\tt generalize \ident$_1$ \dots -% \ident$_n$} (see section \ref{generalize}) then the \texttt{Linear} +% \ident$_n$} (see Section~\ref{generalize}) then the \texttt{Linear} % tactic. So one can use axioms, lemmas or hypotheses of the local % context with \texttt{Linear} in this way. % \end{Variants} @@ -2840,7 +2840,7 @@ formulas built with \verb|~|, \verb|\/|, \verb|/\|, both the type \texttt{nat} of natural numbers and \texttt{Z} of binary integers. This tactic must be loaded by the command \texttt{Require Import Omega}. See the additional documentation about \texttt{omega} -(chapter~\ref{OmegaChapter}). +(see Chapter~\ref{OmegaChapter}). \subsection{{\tt ring} and {\tt ring\_simplify \term$_1$ \dots\ \term$_n$} \tacindex{ring} @@ -2859,7 +2859,7 @@ the terms given in the conclusion of the goal by their normal forms. If no term is given, then the conclusion should be an equation and both hand sides are normalized. -See chapter~\ref{ring} for more information on the tactic and how to +See Chapter~\ref{ring} for more information on the tactic and how to declare new ring structures. \subsection{{\tt field}, {\tt field\_simplify \term$_1$\dots\ \term$_n$} @@ -2885,7 +2885,7 @@ division nor inverse. All of these 3 tactics may generate a subgoal in order to prove that denominators are different from zero. -See chapter~\ref{ring} for more information on the tactic and how to +See Chapter~\ref{ring} for more information on the tactic and how to declare new field structures. \Example @@ -2973,9 +2973,9 @@ $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step. \end{Variant} -\SeeAlso section \ref{HintRewrite} for feeding the database of lemmas used by {\tt autorewrite}. +\SeeAlso Section~\ref{HintRewrite} for feeding the database of lemmas used by {\tt autorewrite}. -\SeeAlso section \ref{autorewrite-example} for examples showing the use of +\SeeAlso Section~\ref{autorewrite-example} for examples showing the use of this tactic. % En attente d'un moyen de valoriser les fichiers de demos @@ -3336,7 +3336,7 @@ e.g. \texttt{Require Import A.}). ``\verb#...#''. In this case the tactic command typed by the user is equivalent to \tac$_1$;{\tac}. -\SeeAlso {\tt Proof.} in section~\ref{BeginProof}. +\SeeAlso {\tt Proof.} in Section~\ref{BeginProof}. \subsubsection[\tt Declare Implicit Tactic {\tac}.]{\tt Declare Implicit Tactic {\tac}.\comindex{Declare Implicit Tactic}} @@ -3480,7 +3480,7 @@ where it was defined. If you want that a tactic macro defined in a module is usable in the modules that require it, you should put it outside of any section. -The chapter~\ref{TacticLanguage} gives examples of more complex +Chapter~\ref{TacticLanguage} gives examples of more complex user-defined tactics. diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index 951de0cd7..9837c8ba3 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -363,7 +363,7 @@ Qed. \end{coq_example*} \Rem There is a difference between obtaining an induction scheme for a -function by using \texttt{Function} (section~\ref{Function}) and by +function by using \texttt{Function} (see Section~\ref{Function}) and by using \texttt{Functional Scheme} after a normal definition using \texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for details. 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. diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 8438a6337..2305fa431 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -132,21 +132,21 @@ the sources of \Coq{} somewhere and have an environment variable named % In the \Coq\ distribution, there is also a separated and independent tool, % called {\sf Coq\_SearchIsos}, which allows the search in accordance with {\tt -% SearchIsos}\index{SearchIsos@{\tt SearchIsos}} (see section~\ref{searchisos}) +% SearchIsos}\index{SearchIsos@{\tt SearchIsos}} (see Section~\ref{searchisos}) % in a \Coq\ proofs library. More precisely, this program begins, once launched % by {\tt coqtop -searchisos}\index{coqtopsearchisos@{\tt % coqtop -searchisos}}, loading lightly (by using specifications functions) % all the \Coq\ objects files ({\tt .vo}) accessible by the {\tt LoadPath} (see -% section~\ref{loadpath}). Next, a prompt appears and four commands are then +% Section~\ref{loadpath}). Next, a prompt appears and four commands are then % available: % \begin{description} % \item [{\tt SearchIsos}]\ \\ % Scans the fixed context. % \item [{\tt Time}]\index{Time@{\tt Time}}\ \\ -% Turns on the Time Search Display mode (see section~\ref{time}). +% Turns on the Time Search Display mode (see Section~\ref{time}). % \item [{\tt Untime}]\index{Untime@{\tt Untime}}\ \\ -% Turns off the Time Search Display mode (see section~\ref{time}). +% Turns off the Time Search Display mode (see Section~\ref{time}). % \item [{\tt Quit}]\index{Quit@{\tt Quit}}\ \\ % Ends the {\tt coqtop -searchisos} session. % \end{description} -- cgit v1.2.3