From 96fb5028a131627f5348bbec315f3b1223837e7b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 25 Jan 2015 18:58:13 +0100 Subject: Doc: Overfull lines in chapter on Canonical Structures. --- doc/refman/CanonicalStructures.tex | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'doc') diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex index c8e36197ca..7b3bdcf4a9 100644 --- a/doc/refman/CanonicalStructures.tex +++ b/doc/refman/CanonicalStructures.tex @@ -309,11 +309,15 @@ We need some infrastructure for that. Require Import Strings.String. Module infrastructure. Inductive phantom {T : Type} (t : T) : Type := Phantom. - Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := phantom t1 -> phantom t2. + Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := + phantom t1 -> phantom t2. Definition id {T} {t : T} (x : phantom t) := x. - Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) (at level 50, v ident, only parsing). - Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) (at level 50, v ident, only parsing). - Notation "'Error : t : s" := (unify _ t (Some s)) (at level 50, format "''Error' : t : s"). + Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) + (at level 50, v ident, only parsing). + Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) + (at level 50, v ident, only parsing). + Notation "'Error : t : s" := (unify _ t (Some s)) + (at level 50, format "''Error' : t : s"). Open Scope string_scope. End infrastructure. \end{coq_example} -- cgit v1.2.3 From 93d7fbf51f9863ce0e1649a221a5e4d3433d3cb6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 29 Jan 2015 11:11:54 +0100 Subject: Fix some broken Coq scripts in the reference manual. --- doc/refman/Misc.tex | 2 +- doc/refman/RefMan-decl.tex | 4 ++-- doc/refman/RefMan-gal.tex | 2 +- doc/refman/RefMan-pro.tex | 10 +++++----- doc/refman/RefMan-tac.tex | 6 +++--- doc/refman/RefMan-tacex.tex | 2 +- 6 files changed, 13 insertions(+), 13 deletions(-) (limited to 'doc') diff --git a/doc/refman/Misc.tex b/doc/refman/Misc.tex index 6ce4ee4801..e953d2f709 100644 --- a/doc/refman/Misc.tex +++ b/doc/refman/Misc.tex @@ -30,7 +30,7 @@ always transparent. \Example \begin{coq_example*} -Require Coq.Derive.Derive. +Require Coq.derive.Derive. Require Import Coq.Numbers.Natural.Peano.NPeano. Section P. diff --git a/doc/refman/RefMan-decl.tex b/doc/refman/RefMan-decl.tex index 292b8bbed2..bafea22d79 100644 --- a/doc/refman/RefMan-decl.tex +++ b/doc/refman/RefMan-decl.tex @@ -381,7 +381,7 @@ thus B by HB. Abort. \end{coq_eval} -The command fails the refinement process cannot find a place to fit +The command fails if the refinement process cannot find a place to fit the object in a proof of the conclusion. @@ -494,7 +494,7 @@ suffices to have x such that HP':(P x) to show B by HP,HP'. Abort. \end{coq_eval} -Finally, an example where {\tt focus} is handy : local assumptions. +Finally, an example where {\tt focus} is handy: local assumptions. \begin{coq_eval} Theorem T: forall (A:Prop) (P:nat -> Prop), P 2 -> A -> A /\ (forall x, x = 2 -> P x). diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 68a2e5dace..0d628ac7ee 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -900,7 +900,7 @@ These are synonyms of the {\tt Definition} forms. \end{Variants} \begin{ErrMsgs} -\item \errindex{Error: The term {\term} has type {\type} while it is expected to have type {\type}} +\item \errindex{The term {\term} has type {\type} while it is expected to have type {\type}} \end{ErrMsgs} \SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}. diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index df707ce941..08213abe9a 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -312,7 +312,7 @@ together with a suggestion about the right bullet or {\tt \}} to unfocus it or focus the next one. \begin{ErrMsgs} -\item \errindex{Error: This proof is focused, but cannot be unfocused +\item \errindex{This proof is focused, but cannot be unfocused this way} You are trying to use {\tt \}} but the current subproof has not been fully solved. \item see also error message about bullets below. @@ -363,25 +363,25 @@ Proof. \begin{ErrMsgs} -\item \errindex{Error: Wrong bullet {\abullet}1 : Current bullet +\item \errindex{Wrong bullet {\abullet}1 : Current bullet {\abullet}2 is not finished.} Before using bullet {\abullet}1 again, you should first finish proving the current focused goal. Note that {\abullet}1 and {\abullet}2 may be the same. -\item \errindex{Error: Wrong bullet {\abullet}1 : Bullet {\abullet}2 +\item \errindex{Wrong bullet {\abullet}1 : Bullet {\abullet}2 is mandatory here.} You must put {\abullet}2 to focus next goal. No other bullet is allowed here. -\item \errindex{Error: No such goal. Focus next goal with bullet +\item \errindex{No such goal. Focus next goal with bullet {\abullet}.} You tried to applied a tactic but no goal where under focus. Using {\abullet} is mandatory here. -\item \errindex{Error: No such goal. Try unfocusing with "{\tt \}}".} You +\item \errindex{No such goal. Try unfocusing with {"{\tt \}}"}.} You just finished a goal focused by {\tt \{}, you must unfocus it with "{\tt \}}". \end{ErrMsgs} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 35da17d546..dcc2bcc1f6 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -65,8 +65,8 @@ make is so that tactics are, by default, applied to every goal simultaneously. Then, to apply a tactic {\tt tac} to the first goal only, you can write {\tt 1:tac}. -\subsection[\tt Test Default Goal Selector ``\selector''.] - {\tt Test Default Goal Selector ``\selector''. +\subsection[\tt Test Default Goal Selector.] + {\tt Test Default Goal Selector. \comindex{Test Default Goal Selector}} This command displays the current default selector. @@ -2029,7 +2029,7 @@ Import Nat. Functional Scheme minus_ind := Induction for minus Sort Prop. Check minus_ind. Lemma le_minus (n m:nat) : n - m <= n. -functional induction (minus n m); simpl; auto. +functional induction (minus n m) using minus_ind; simpl; auto. \end{coq_example} \begin{coq_example*} Qed. diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index 5703c73f02..668a68c9c7 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -164,7 +164,7 @@ Notation " t --> t' " := (arrow t t') (at level 20, t' at next level). Inductive ctx : Type := | empty : ctx | snoc : ctx -> type -> ctx. -Notation " G , tau " := (snoc G tau) (at level 20, t at next level). +Notation " G , tau " := (snoc G tau) (at level 20, tau at next level). Fixpoint conc (G D : ctx) : ctx := match D with | empty => G -- cgit v1.2.3 From 266d837f79c908af0cfcf9684f16b17a9c1d5cfb Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 29 Jan 2015 11:37:21 +0100 Subject: Fix some typos in the documentation. --- doc/refman/RefMan-decl.tex | 77 +++++++++++++++++++++++++++------------------- 1 file changed, 46 insertions(+), 31 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-decl.tex b/doc/refman/RefMan-decl.tex index bafea22d79..c84e3a9dfa 100644 --- a/doc/refman/RefMan-decl.tex +++ b/doc/refman/RefMan-decl.tex @@ -16,7 +16,7 @@ The intent is to provide language where proofs are less formalism-{} and implementation-{}sensitive, and in the process to ease a bit the learning of computer-{}aided proof verification. -\subsection{What is a declarative proof ?{}} +\subsection{What is a declarative proof?} In vanilla Coq, proofs are written in the imperative style: the user issues commands that transform a so called proof state until it reaches a state where the proof is completed. In the process, the user @@ -48,7 +48,7 @@ correct: \subsection{Note for tactics users} This section explain what differences the casual Coq user will -experience using the \DPL . +experience using the \DPL. \begin{enumerate} \item The focusing mechanism is constrained so that only one goal at a time is visible. @@ -77,7 +77,7 @@ However it is not supported by structured editors such as PCoq. \section{Syntax} -Here is a complete formal description of the syntax for DPL commands. +Here is a complete formal description of the syntax for \DPL{} commands. \begin{figure}[htbp] \begin{centerframe} @@ -127,7 +127,7 @@ The lexical conventions used here follows those of section \ref{lexical}. Conventions:\begin{itemize} - \item {\texttt{<{}tactic>{}}} stands for an Coq tactic. + \item {\texttt{<{}tactic>{}}} stands for a Coq tactic. \end{itemize} @@ -135,7 +135,7 @@ Conventions:\begin{itemize} In proof commands where an optional name is asked for, omitting the name will trigger the creation of a fresh temporary name (e.g. for a -hypothesis). Temporary names always start with an undescore '\_' +hypothesis). Temporary names always start with an underscore `\_' character (e.g. {\tt \_hyp0}). Temporary names have a lifespan of one command: they get erased after the next command. They can however be safely in the step after their creation. @@ -143,7 +143,12 @@ command: they get erased after the next command. They can however be safely in t \subsection{Starting and Ending a mathematical proof} - The standard way to use the \DPL is to first state a {\texttt{Lemma/Theorem/Definition}} and then use the {\texttt{proof}} command to switch the current subgoal to mathematical mode. After the proof is completed, the {\texttt{end proof}} command will close the mathematical proof. If any subgoal remains to be proved, they will be displayed using the usual Coq display. +The standard way to use the \DPL{} is to first state a \texttt{Lemma} / +\texttt{Theorem} / \texttt{Definition} and then use the \texttt{proof} +command to switch the current subgoal to mathematical mode. After the +proof is completed, the \texttt{end proof} command will close the +mathematical proof. If any subgoal remains to be proved, they will be +displayed using the usual Coq display. \begin{coq_example} Theorem this_is_trivial: True. @@ -154,13 +159,13 @@ Qed. \end{coq_example} The {\texttt{proof}} command only applies to \emph{one subgoal}, thus -if several sub-goals are already present, the {\texttt{proof .. end +if several sub-goals are already present, the {\texttt{proof ... end proof}} sequence has to be used several times. -\begin{coq_eval} +\begin{coq_example*} Theorem T: (True /\ True) /\ True. split. split. -\end{coq_eval} +\end{coq_example*} \begin{coq_example} Show. proof. (* first subgoal *) @@ -187,7 +192,7 @@ later. Theorem this_is_not_so_trivial: False. proof. end proof. (* here a warning is issued *) -Qed. (* fails : the proof in incomplete *) +Qed. (* fails: the proof in incomplete *) Admitted. (* Oops! *) \end{coq_example} \begin{coq_eval} @@ -220,7 +225,7 @@ warning is issued and the proof cannot be saved anymore. It is possible to use the {\texttt{proof}} command inside an {\texttt{escape...return}} block, thus nesting a mathematical proof -inside a procedural proof inside a mathematical proof ... +inside a procedural proof inside a mathematical proof... \subsection{Computation steps} @@ -244,8 +249,10 @@ Abort. \subsection{Deduction steps} -The most common instruction in a mathematical proof is the deduction step: - it asserts a new statement (a formula/type of the \CIC) and tries to prove it using a user-provided indication : the justification. The asserted statement is then added as a hypothesis to the proof context. +The most common instruction in a mathematical proof is the deduction +step: it asserts a new statement (a formula/type of the \CIC) and tries +to prove it using a user-provided indication: the justification. The +asserted statement is then added as a hypothesis to the proof context. \begin{coq_eval} Theorem T: forall x, x=2 -> 2+x=4. @@ -260,7 +267,9 @@ let x be such that H:(x=2). Abort. \end{coq_eval} -It is very often the case that the justifications uses the last hypothesis introduced in the context, so the {\tt then} keyword can be used as a shortcut, e.g. if we want to do the same as the last example : +It is often the case that the justifications uses the last hypothesis +introduced in the context, so the {\tt then} keyword can be used as a +shortcut, e.g. if we want to do the same as the last example: \begin{coq_eval} Theorem T: forall x, x=2 -> 2+x=4. @@ -279,7 +288,7 @@ In this example, you can also see the creation of a temporary name {\tt \_fact}. \subsection{Iterated equalities} -A common proof pattern when doing a chain of deductions, is to do +A common proof pattern when doing a chain of deductions is to do multiple rewriting steps over the same term, thus proving the corresponding equalities. The iterated equalities are a syntactic support for this kind of reasoning: @@ -305,7 +314,10 @@ Notice that here we use temporary names heavily. \subsection{Subproofs} -When an intermediate step in a proof gets too complicated or involves a well contained set of intermediate deductions, it can be useful to insert its proof as a subproof of the current proof. this is done by using the {\tt claim ... end claim} pair of commands. +When an intermediate step in a proof gets too complicated or involves a +well contained set of intermediate deductions, it can be useful to insert +its proof as a subproof of the current proof. This is done by using the +{\tt claim ... end claim} pair of commands. \begin{coq_eval} Theorem T: forall x, x + x = x * x -> x = 0 \/ x = 2. @@ -317,7 +329,7 @@ Show. claim H':((x - 2) * x = 0). \end{coq_example} -A few steps later ... +A few steps later... \begin{coq_example} thus thesis. @@ -350,7 +362,7 @@ conclusion step & {\tt thus} & {\tt hence} & \caption{Correspondence between basic forward steps and conclusion steps} \end{figure} -Let us begin with simple examples : +Let us begin with simple examples: \begin{coq_eval} Theorem T: forall (A B:Prop), A -> B -> A /\ B. @@ -518,7 +530,7 @@ In order to shorten long expressions, it is possible to use the {\tt define ... as ...} command to give a name to recurring expressions. \begin{coq_eval} -Theorem T: forall x, x = 0 -> x + x = x * x . +Theorem T: forall x, x = 0 -> x + x = x * x. proof. let x be such that H:(x = 0). \end{coq_eval} @@ -534,10 +546,12 @@ Abort. \subsection{Introduction steps} When the {\tt thesis} consists of a hypothetical formula (implication -or universal quantification (e.g. \verb+A -> B+) , it is possible to +or universal quantification (e.g. \verb+A -> B+), it is possible to assume the hypothetical part {\tt A} and then prove {\tt B}. In the \DPL{}, this comes in two syntactic flavors that are semantically -equivalent : {\tt let} and {\tt assume}. Their syntax is designed so that {\tt let} works better for universal quantifiers and {\tt assume} for implications. +equivalent: {\tt let} and {\tt assume}. Their syntax is designed so that +{\tt let} works better for universal quantifiers and {\tt assume} for +implications. \begin{coq_eval} Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. @@ -571,7 +585,8 @@ let x be such that HP:(P x). (* here x's type is inferred from (P x) *) Abort. \end{coq_eval} -In the {\tt assume } variant, the type of the assumed object is mandatory but the name is optional : +In the {\tt assume } variant, the type of the assumed object is mandatory +but the name is optional: \begin{coq_eval} Theorem T: forall (P:nat -> Prop), forall x, P x -> P x -> P x. @@ -587,7 +602,7 @@ assume (P x). (* temporary name created *) Abort. \end{coq_eval} -After {\tt such that}, it is also the case : +After {\tt such that}, it is also the case: \begin{coq_eval} Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. @@ -604,8 +619,8 @@ Abort. \subsection{Tuple elimination steps} -In the \CIC, many objects dealt with in simple proofs are tuples : -pairs , records, existentially quantified formulas. These are so +In the \CIC, many objects dealt with in simple proofs are tuples: +pairs, records, existentially quantified formulas. These are so common that the \DPL{} provides a mechanism to extract members of those tuples, and also objects in tuples within tuples within tuples... @@ -613,7 +628,7 @@ tuples... \begin{coq_eval} Theorem T: forall (P:nat -> Prop) (A:Prop), (exists x, (P x /\ A)) -> A. proof. -let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A) . +let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A). \end{coq_eval} \begin{coq_example} Show. @@ -643,10 +658,10 @@ It is sometimes desirable to combine assumption and tuple decomposition. This can be done using the {\tt given} command. \begin{coq_eval} -Theorem T: forall P:(nat -> Prop), (forall n , P n -> P (n - 1)) -> +Theorem T: forall P:(nat -> Prop), (forall n, P n -> P (n - 1)) -> (exists m, P m) -> P 0. proof. -let P:(nat -> Prop) be such that HP:(forall n , P n -> P (n - 1)). +let P:(nat -> Prop) be such that HP:(forall n, P n -> P (n - 1)). \end{coq_eval} \begin{coq_example} Show. @@ -687,7 +702,7 @@ The proof is well formed (but incomplete) even if you type {\tt end If the disjunction is derived from a more general principle, e.g. the excluded middle axiom), it is desirable to just specify which instance -of it is being used : +of it is being used: \begin{coq_eval} Section Coq. @@ -789,14 +804,14 @@ Intuitively, justifications are hints for the system to understand how to prove the statements the user types in. In the case of this language justifications are made of two components: -Justification objects : {\texttt{by}} followed by a comma-{}separated +Justification objects: {\texttt{by}} followed by a comma-{}separated list of objects that will be used by a selected tactic to prove the statement. This defaults to the empty list (the statement should then be tautological). The * wildcard provides the usual tactics behavior: use all statements in local context. However, this wildcard should be avoided since it reduces the robustness of the script. -Justification tactic : {\texttt{using}} followed by a Coq tactic that +Justification tactic: {\texttt{using}} followed by a Coq tactic that is executed to prove the statement. The default is a solver for (intuitionistic) first-{}order with equality. -- cgit v1.2.3 From fe038eea4f1c62a209db18fadb69dbab80e16c16 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 29 Jan 2015 15:07:12 +0100 Subject: Remove some "Warning:" from the reference manual. --- doc/refman/Cases.tex | 49 ++++++++++++++++++++++++++++------------------- doc/refman/RefMan-ext.tex | 2 +- doc/refman/RefMan-mod.tex | 2 +- 3 files changed, 31 insertions(+), 22 deletions(-) (limited to 'doc') diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex index 7e01edeb0d..51ec2ef818 100644 --- a/doc/refman/Cases.tex +++ b/doc/refman/Cases.tex @@ -77,8 +77,10 @@ Fixpoint max (n m:nat) {struct m} : nat := Using multiple patterns in the definition of {\tt max} lets us write: -\begin{coq_example} +\begin{coq_eval} Reset max. +\end{coq_eval} +\begin{coq_example} Fixpoint max (n m:nat) {struct m} : nat := match n, m with | O, _ => m @@ -105,8 +107,10 @@ Check (fun x:nat => match x return nat with We can also use ``\texttt{as} {\ident}'' to associate a name to a sub-pattern: -\begin{coq_example} +\begin{coq_eval} Reset max. +\end{coq_eval} +\begin{coq_example} Fixpoint max (n m:nat) {struct n} : nat := match n, m with | O, _ => m @@ -133,8 +137,10 @@ This is compiled into: \begin{coq_example} Unset Printing Matching. Print even. -Set Printing Matching. \end{coq_example} +\begin{coq_eval} +Set Printing Matching. +\end{coq_eval} In the previous examples patterns do not conflict with, but sometimes it is comfortable to write patterns that admit a non @@ -164,8 +170,10 @@ yields \texttt{true}. Another way to write this function is: -\begin{coq_example} +\begin{coq_eval} Reset lef. +\end{coq_eval} +\begin{coq_example} Fixpoint lef (n m:nat) {struct m} : bool := match n, m with | O, x => true @@ -181,11 +189,9 @@ the second one. Terms with useless patterns are not accepted by the system. Here is an example: -% Test failure +% Test failure: "This clause is redundant." \begin{coq_eval} Set Printing Depth 50. - (********** The following is not correct and should produce **********) - (**************** Error: This clause is redundant ********************) \end{coq_eval} \begin{coq_example} Check (fun x:nat => @@ -260,11 +266,9 @@ Check When we use parameters in patterns there is an error message: -% Test failure +% Test failure: "The parameters do not bind in patterns." \begin{coq_eval} Set Printing Depth 50. -(********** The following is not correct and should produce **********) -(******** Error: Parameters do not bind ... ************) \end{coq_eval} \begin{coq_example} Check @@ -324,8 +328,10 @@ Definition length (n:nat) (l:listn n) := n. Just for illustrating pattern matching, we can define it by case analysis: -\begin{coq_example} +\begin{coq_eval} Reset length. +\end{coq_eval} +\begin{coq_example} Definition length (n:nat) (l:listn n) := match l with | niln => 0 @@ -454,8 +460,10 @@ introduce a dependent product. For example, an equivalent definition for \texttt{concat} (even though the matching on the second term is trivial) would have been: -\begin{coq_example} +\begin{coq_eval} Reset concat. +\end{coq_eval} +\begin{coq_example} Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : listn (n + m) := match l in listn n, l' return listn (n + m) with @@ -517,17 +525,18 @@ If the type of the matched term is more precise than an inductive applied to variables, arguments of the inductive in the {\tt in} branch can be more complicated patterns than a variable. -Moreover, constructors whose type do not follow the same pattern will become -impossible branch. In impossible branch, you can answer anything but {\tt - False\_rect unit} has the advantage to be subterm of anything. +Moreover, constructors whose type do not follow the same pattern will +become impossible branches. In an impossible branch, you can answer +anything but {\tt False\_rect unit} has the advantage to be subterm of +anything. % ??? To be concrete: the tail function can be written: \begin{coq_example} - Definition tail n (v: listn (S n)) := - match v in listn (S m) return listn m with - | niln => False_rect unit - | consn n' a y => y - end. +Definition tail n (v: listn (S n)) := + match v in listn (S m) return listn m with + | niln => False_rect unit + | consn n' a y => y + end. \end{coq_example} and {\tt tail n v} will be subterm of {\tt v}. diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 193479cceb..4b197ec738 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -167,7 +167,7 @@ defined with the {\tt Record} keyword can be activated with the (see~\ref{set-nonrecursive-elimination-schemes}). \begin{Warnings} -\item {\tt Warning: {\ident$_i$} cannot be defined.} +\item {\tt {\ident$_i$} cannot be defined.} It can happen that the definition of a projection is impossible. This message is followed by an explanation of this impossibility. diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index 505c1110c7..0e7b39c751 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -403,7 +403,7 @@ Check B.T. \end{ErrMsgs} \begin{Warnings} - \item Warning: Trying to mask the absolute name {\qualid} ! + \item Trying to mask the absolute name {\qualid} ! \end{Warnings} \subsection{\tt Print Module {\ident} -- cgit v1.2.3 From 1dfcae672aa1630bb1fe841bae9321dd9f221fc4 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 29 Jan 2015 15:27:49 +0100 Subject: Remove spurious "Loading ML file" and " Grammar extension" from the reference manual. --- doc/refman/CanonicalStructures.tex | 4 +- doc/refman/Polynom.tex | 115 +++++++++++++++++++------------------ doc/refman/RefMan-lib.tex | 8 ++- doc/refman/RefMan-oth.tex | 5 +- 4 files changed, 72 insertions(+), 60 deletions(-) (limited to 'doc') diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex index 7b3bdcf4a9..b1c278cede 100644 --- a/doc/refman/CanonicalStructures.tex +++ b/doc/refman/CanonicalStructures.tex @@ -305,8 +305,10 @@ canonical structures. We need some infrastructure for that. -\begin{coq_example} +\begin{coq_example*} Require Import Strings.String. +\end{coq_example*} +\begin{coq_example} Module infrastructure. Inductive phantom {T : Type} (t : T) : Type := Phantom. Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex index 974a562470..0664bf9095 100644 --- a/doc/refman/Polynom.tex +++ b/doc/refman/Polynom.tex @@ -122,8 +122,10 @@ for \texttt{N}, do \texttt{Require Import NArithRing} or \begin{coq_eval} Reset Initial. \end{coq_eval} -\begin{coq_example} +\begin{coq_example*} Require Import ZArith. +\end{coq_example*} +\begin{coq_example} Open Scope Z_scope. Goal forall a b c:Z, (a + b + c)^2 = @@ -193,28 +195,28 @@ also supported. The equality can be either Leibniz equality, or any relation declared as a setoid (see~\ref{setoidtactics}). The definition of ring and semi-rings (see module {\tt Ring\_theory}) is: \begin{verbatim} - Record ring_theory : Prop := mk_rt { - Radd_0_l : forall x, 0 + x == x; - Radd_sym : forall x y, x + y == y + x; - Radd_assoc : forall x y z, x + (y + z) == (x + y) + z; - Rmul_1_l : forall x, 1 * x == x; - Rmul_sym : forall x y, x * y == y * x; - Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z; - Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); - Rsub_def : forall x y, x - y == x + -y; - Ropp_def : forall x, x + (- x) == 0 - }. +Record ring_theory : Prop := mk_rt { + Radd_0_l : forall x, 0 + x == x; + Radd_sym : forall x y, x + y == y + x; + Radd_assoc : forall x y z, x + (y + z) == (x + y) + z; + Rmul_1_l : forall x, 1 * x == x; + Rmul_sym : forall x y, x * y == y * x; + Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z; + Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); + Rsub_def : forall x y, x - y == x + -y; + Ropp_def : forall x, x + (- x) == 0 +}. Record semi_ring_theory : Prop := mk_srt { - SRadd_0_l : forall n, 0 + n == n; - SRadd_sym : forall n m, n + m == m + n ; - SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p; - SRmul_1_l : forall n, 1*n == n; - SRmul_0_l : forall n, 0*n == 0; - SRmul_sym : forall n m, n*m == m*n; - SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p; - SRdistr_l : forall n m p, (n + m)*p == n*p + m*p - }. + SRadd_0_l : forall n, 0 + n == n; + SRadd_sym : forall n m, n + m == m + n ; + SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p; + SRmul_1_l : forall n, 1*n == n; + SRmul_0_l : forall n, 0*n == 0; + SRmul_sym : forall n m, n*m == m*n; + SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p; + SRdistr_l : forall n m p, (n + m)*p == n*p + m*p +}. \end{verbatim} This implementation of {\tt ring} also features a notion of constant @@ -230,23 +232,23 @@ could be the rational numbers, upon which the ring operations can be implemented. The fact that there exists a morphism is defined by the following properties: \begin{verbatim} - Record ring_morph : Prop := mkmorph { - morph0 : [cO] == 0; - morph1 : [cI] == 1; - morph_add : forall x y, [x +! y] == [x]+[y]; - morph_sub : forall x y, [x -! y] == [x]-[y]; - morph_mul : forall x y, [x *! y] == [x]*[y]; - morph_opp : forall x, [-!x] == -[x]; - morph_eq : forall x y, x?=!y = true -> [x] == [y] - }. +Record ring_morph : Prop := mkmorph { + morph0 : [cO] == 0; + morph1 : [cI] == 1; + morph_add : forall x y, [x +! y] == [x]+[y]; + morph_sub : forall x y, [x -! y] == [x]-[y]; + morph_mul : forall x y, [x *! y] == [x]*[y]; + morph_opp : forall x, [-!x] == -[x]; + morph_eq : forall x y, x?=!y = true -> [x] == [y] +}. - Record semi_morph : Prop := mkRmorph { - Smorph0 : [cO] == 0; - Smorph1 : [cI] == 1; - Smorph_add : forall x y, [x +! y] == [x]+[y]; - Smorph_mul : forall x y, [x *! y] == [x]*[y]; - Smorph_eq : forall x y, x?=!y = true -> [x] == [y] - }. +Record semi_morph : Prop := mkRmorph { + Smorph0 : [cO] == 0; + Smorph1 : [cI] == 1; + Smorph_add : forall x y, [x +! y] == [x]+[y]; + Smorph_mul : forall x y, [x *! y] == [x]*[y]; + Smorph_eq : forall x y, x?=!y = true -> [x] == [y] +}. \end{verbatim} where {\tt c0} and {\tt cI} denote the 0 and 1 of the coefficient set, {\tt +!}, {\tt *!}, {\tt -!} are the implementations of the ring @@ -274,16 +276,16 @@ This implementation of ring can also recognize simple power expressions as ring expressions. A power function is specified by the following property: \begin{verbatim} - Section POWER. +Section POWER. Variable Cpow : Set. Variable Cp_phi : N -> Cpow. - Variable rpow : R -> Cpow -> R. - + Variable rpow : R -> Cpow -> R. + Record power_theory : Prop := mkpow_th { rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n) }. - End POWER. +End POWER. \end{verbatim} @@ -398,7 +400,7 @@ Polynomials in normal form are defined as: \begin{small} \begin{flushleft} \begin{verbatim} - Inductive Pol : Type := +Inductive Pol : Type := | Pc : C -> Pol | Pinj : positive -> Pol -> Pol | PX : Pol -> positive -> Pol -> Pol. @@ -501,8 +503,10 @@ field in module \texttt{Qcanon}. \begin{coq_eval} Reset Initial. \end{coq_eval} -\begin{coq_example} +\begin{coq_example*} Require Import Reals. +\end{coq_example*} +\begin{coq_example} Open Scope R_scope. Goal forall x, x <> 0 -> (1 - 1/x) * x - x + 1 = 0. @@ -600,17 +604,17 @@ relation declared as a setoid (see~\ref{setoidtactics}). The definition of fields and semi-fields is: \begin{verbatim} Record field_theory : Prop := mk_field { - F_R : ring_theory rO rI radd rmul rsub ropp req; - F_1_neq_0 : ~ 1 == 0; - Fdiv_def : forall p q, p / q == p * / q; - Finv_l : forall p, ~ p == 0 -> / p * p == 1 + F_R : ring_theory rO rI radd rmul rsub ropp req; + F_1_neq_0 : ~ 1 == 0; + Fdiv_def : forall p q, p / q == p * / q; + Finv_l : forall p, ~ p == 0 -> / p * p == 1 }. Record semi_field_theory : Prop := mk_sfield { - SF_SR : semi_ring_theory rO rI radd rmul req; - SF_1_neq_0 : ~ 1 == 0; - SFdiv_def : forall p q, p / q == p * / q; - SFinv_l : forall p, ~ p == 0 -> / p * p == 1 + SF_SR : semi_ring_theory rO rI radd rmul req; + SF_1_neq_0 : ~ 1 == 0; + SFdiv_def : forall p q, p / q == p * / q; + SFinv_l : forall p, ~ p == 0 -> / p * p == 1 }. \end{verbatim} @@ -618,9 +622,10 @@ The result of the normalization process is a fraction represented by the following type: \begin{verbatim} Record linear : Type := mk_linear { - num : PExpr C; - denum : PExpr C; - condition : list (PExpr C) }. + num : PExpr C; + denum : PExpr C; + condition : list (PExpr C) +}. \end{verbatim} where {\tt num} and {\tt denum} are the numerator and denominator; {\tt condition} is a list of expressions that have appeared as a @@ -661,7 +666,7 @@ intros; rewrite (Z.mul_comm y z); reflexivity. Save toto. \end{coq_example*} \begin{coq_example} -Print toto. +Print toto. \end{coq_example} At each step of rewriting, the whole context is duplicated in the proof diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index 49382f3e20..7227f4b7b6 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -892,8 +892,10 @@ Figure~\ref{zarith-syntax} shows the notations provided by {\tt Z\_scope}. It specifies how notations are interpreted and, when not already reserved, the precedence and associativity. -\begin{coq_example} +\begin{coq_example*} Require Import ZArith. +\end{coq_example*} +\begin{coq_example} Check (2 + 3)%Z. Open Scope Z_scope. Check 2 + 3. @@ -968,8 +970,10 @@ Notation & Interpretation \\ \begin{coq_eval} Reset Initial. \end{coq_eval} -\begin{coq_example} +\begin{coq_example*} Require Import Reals. +\end{coq_example*} +\begin{coq_example} Check (2 + 3)%R. Open Scope R_scope. Check 2 + 3. diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 64fab055ea..ce230a0f73 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -355,8 +355,10 @@ is a variant of {\tt Search statements whose conclusion has exactly the expected form, or whose statement finishes by the given series of hypothesis/conclusion. -\begin{coq_example} +\begin{coq_example*} Require Import Arith. +\end{coq_example*} +\begin{coq_example} SearchPattern (_ + _ = _ + _). SearchPattern (nat -> bool). SearchPattern (forall l : list _, _ l l). @@ -367,7 +369,6 @@ must occur in two places by using pattern variables `{\texttt ?{\ident}}''. \begin{coq_example} -Require Import Arith. SearchPattern (?X1 + _ = _ + ?X1). \end{coq_example} -- cgit v1.2.3 From db293d185f8deb091d4b086f327caa0f376d67d7 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 29 Jan 2015 20:04:22 +0100 Subject: Fix index of reference manual. --- doc/refman/RefMan-com.tex | 3 +- doc/refman/RefMan-ext.tex | 4 +-- doc/refman/RefMan-ltac.tex | 75 ++++++++++++++++++++++++---------------------- doc/refman/RefMan-syn.tex | 2 +- doc/refman/RefMan-uti.tex | 20 ++++++------- doc/refman/coqdoc.tex | 5 ++-- 6 files changed, 57 insertions(+), 52 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index a937332569..49bcdb1db7 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -1,6 +1,7 @@ \chapter[The \Coq~commands]{The \Coq~commands\label{Addoc-coqc} \ttindex{coqtop} -\ttindex{coqc}} +\ttindex{coqc} +\ttindex{coqchk}} There are three \Coq~commands: \begin{itemize} diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 4b197ec738..3605a716e7 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -434,7 +434,7 @@ we have an equivalence between {\tt match {\term} \zeroone{\ifitem} with C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end} -\subsubsection{Second destructuring {\tt let} syntax\index{let '... in}} +\subsubsection{Second destructuring {\tt let} syntax\index{let '... in@\texttt{let '... in}}} Another destructuring {\tt let} syntax is available for inductive types with one constructor by giving an arbitrary pattern instead of just a tuple @@ -2000,7 +2000,7 @@ variables, use \end{quote} \subsection{Solving existential variables using tactics} -\index{\tt \textdollar( \ldots )\textdollar} +\ttindex{\textdollar( \ldots )\textdollar} \def\expr{\textrm{\textsl{tacexpr}}} diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index de8c26943c..689ac14254 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -620,10 +620,10 @@ runs is displayed. Time is in seconds and is machine-dependent. The {\qstring} argument is optional. When provided, it is used to identify this particular occurrence of {\tt time}. -\subsubsection[Local definitions]{Local definitions\index{Ltac!let} -\index{Ltac!let rec} -\index{let!in Ltac} -\index{let rec!in Ltac}} +\subsubsection[Local definitions]{Local definitions\index{Ltac!let@\texttt{let}} +\index{Ltac!let rec@\texttt{let rec}} +\index{let@\texttt{let}!in Ltac} +\index{let rec@\texttt{let rec}!in Ltac}} Local definitions can be done as follows: \begin{quote} @@ -659,8 +659,8 @@ definition expecting at least $n$ arguments. The expressions %\subsection{Application of tactic values} -\subsubsection[Function construction]{Function construction\index{fun!in Ltac} -\index{Ltac!fun}} +\subsubsection[Function construction]{Function construction\index{fun@\texttt{fun}!in Ltac} +\index{Ltac!fun@\texttt{fun}}} A parameterized tactic can be built anonymously (without resorting to local definitions) with: @@ -670,8 +670,8 @@ local definitions) with: Indeed, local definitions of functions are a syntactic sugar for binding a {\tt fun} tactic to an identifier. -\subsubsection[Pattern matching on terms]{Pattern matching on terms\index{Ltac!match} -\index{match!in Ltac}} +\subsubsection[Pattern matching on terms]{Pattern matching on terms\index{Ltac!match@\texttt{match}} +\index{match@\texttt{match}!in Ltac}} We can carry out pattern matching on terms with: \begin{quote} @@ -729,8 +729,8 @@ it has backtracking points. \begin{Variants} -\item \index{multimatch!in Ltac} -\index{Ltac!multimatch} +\item \index{multimatch@\texttt{multimatch}!in Ltac} +\index{Ltac!multimatch@\texttt{multimatch}} Using {\tt multimatch} instead of {\tt match} will allow subsequent tactics to backtrack into a right-hand side tactic which has backtracking points left and trigger the selection of a new matching @@ -740,8 +740,8 @@ been consumed. The syntax {\tt match \ldots} is, in fact, a shorthand for {\tt once multimatch \ldots}. -\item \index{lazymatch!in Ltac} -\index{Ltac!lazymatch} +\item \index{lazymatch@\texttt{lazymatch}!in Ltac} +\index{Ltac!lazymatch@\texttt{lazymatch}} Using {\tt lazymatch} instead of {\tt match} will perform the same pattern matching procedure but will commit to the first matching branch rather than trying a new matching if the right-hand side @@ -749,7 +749,7 @@ fails. If the right-hand side of the selected branch is a tactic with backtracking points, then subsequent failures cause this tactic to backtrack. -\item \index{context!in pattern} +\item \index{context@\texttt{context}!in pattern} There is a special form of patterns to match a subterm against the pattern: \begin{quote} @@ -778,7 +778,7 @@ Goal True. f (3+4). \end{coq_example} -\item \index{appcontext!in pattern} +\item \index{appcontext@\texttt{appcontext}!in pattern} \comindex{Set Tactic Compat Context} \comindex{Unset Tactic Compat Context} For historical reasons, {\tt context} used to consider $n$-ary applications @@ -796,10 +796,10 @@ behavior can be retrieved with the {\tt Tactic Compat Context} flag. \end{Variants} -\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal} -\index{Ltac!match reverse goal} -\index{match goal!in Ltac} -\index{match reverse goal!in Ltac}} +\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}} +\index{Ltac!match reverse goal@\texttt{match reverse goal}} +\index{match goal@\texttt{match goal}!in Ltac} +\index{match reverse goal@\texttt{match reverse goal}!in Ltac}} We can make pattern matching on goals using the following expression: \begin{quote} @@ -854,10 +854,10 @@ the {\tt match reverse goal with} variant. \variant -\index{multimatch goal!in Ltac} -\index{Ltac!multimatch goal} -\index{multimatch reverse goal!in Ltac} -\index{Ltac!multimatch reverse goal} +\index{multimatch goal@\texttt{multimatch goal}!in Ltac} +\index{Ltac!multimatch goal@\texttt{multimatch goal}} +\index{multimatch reverse goal@\texttt{multimatch reverse goal}!in Ltac} +\index{Ltac!multimatch reverse goal@\texttt{multimatch reverse goal}} Using {\tt multimatch} instead of {\tt match} will allow subsequent tactics to backtrack into a right-hand side tactic which has @@ -868,10 +868,10 @@ of the right-hand side have been consumed. The syntax {\tt match [reverse] goal \ldots} is, in fact, a shorthand for {\tt once multimatch [reverse] goal \ldots}. -\index{lazymatch goal!in Ltac} -\index{Ltac!lazymatch goal} -\index{lazymatch reverse goal!in Ltac} -\index{Ltac!lazymatch reverse goal} +\index{lazymatch goal@\texttt{lazymatch goal}!in Ltac} +\index{Ltac!lazymatch goal@\texttt{lazymatch goal}} +\index{lazymatch reverse goal@\texttt{lazymatch reverse goal}!in Ltac} +\index{Ltac!lazymatch reverse goal@\texttt{lazymatch reverse goal}} Using {\tt lazymatch} instead of {\tt match} will perform the same pattern matching procedure but will commit to the first matching branch with the first matching combination of hypotheses rather than @@ -879,7 +879,7 @@ trying a new matching if the right-hand side fails. If the right-hand side of the selected branch is a tactic with backtracking points, then subsequent failures cause this tactic to backtrack. -\subsubsection[Filling a term context]{Filling a term context\index{context!in expression}} +\subsubsection[Filling a term context]{Filling a term context\index{context@\texttt{context}!in expression}} The following expression is not a tactic in the sense that it does not produce subgoals but generates a term to be used in tactic @@ -895,8 +895,8 @@ replaces the hole of the value of {\ident} by the value of \ErrMsg \errindex{not a context variable} -\subsubsection[Generating fresh hypothesis names]{Generating fresh hypothesis names\index{Ltac!fresh} -\index{fresh!in Ltac}} +\subsubsection[Generating fresh hypothesis names]{Generating fresh hypothesis names\index{Ltac!fresh@\texttt{fresh}} +\index{fresh@\texttt{fresh}!in Ltac}} Tactics sometimes have to generate new names for hypothesis. Letting the system decide a name with the {\tt intro} tactic is not so good @@ -913,8 +913,8 @@ has to refer to a name, or directly a name denoted by a with a number so that it becomes fresh. If no component is given, the name is a fresh derivative of the name {\tt H}. -\subsubsection[Computing in a constr]{Computing in a constr\index{Ltac!eval} -\index{eval!in Ltac}} +\subsubsection[Computing in a constr]{Computing in a constr\index{Ltac!eval@\texttt{eval}} +\index{eval@\texttt{eval}!in Ltac}} Evaluation of a term can be performed with: \begin{quote} @@ -926,8 +926,8 @@ hnf}, {\tt compute}, {\tt simpl}, {\tt cbv}, {\tt lazy}, {\tt unfold}, \subsubsection{Recovering the type of a term} %\tacindex{type of} -\index{Ltac!type of} -\index{type of!in Ltac} +\index{Ltac!type of@\texttt{type of}} +\index{type of@\texttt{type of}!in Ltac} The following returns the type of {\term}: @@ -935,7 +935,10 @@ The following returns the type of {\term}: {\tt type of} {\term} \end{quote} -\subsubsection[Manipulating untyped terms]{Manipulating untyped terms\index{Ltac!uconstr}\index{uconstr!in Ltac}\index{Ltac!type\_term}\index{type\_term!in Ltac}} +\subsubsection[Manipulating untyped terms]{Manipulating untyped terms\index{Ltac!uconstr@\texttt{uconstr}} +\index{uconstr@\texttt{uconstr}!in Ltac} +\index{Ltac!type\_term@\texttt{type\_term}} +\index{type\_term@\texttt{type\_term}!in Ltac}} The terms built in Ltac are well-typed by default. It may not be appropriate for building large terms using a recursive Ltac function: @@ -963,7 +966,7 @@ untyped term is type checked against the conclusion of the goal, and the holes which are not solved by the typing procedure are turned into new subgoals. -\subsubsection[Counting the goals]{Counting the goals\index{Ltac!numgoals}\index{numgoals!in Ltac}} +\subsubsection[Counting the goals]{Counting the goals\index{Ltac!numgoals@\texttt{numgoals}}\index{numgoals@\texttt{numgoals}!in Ltac}} The number of goals under focus can be recovered using the {\tt numgoals} function. Combined with the {\tt guard} command below, it @@ -979,7 +982,7 @@ split;[|split]. all:pr_numgoals. \end{coq_example} -\subsubsection[Testing boolean expressions]{Testing boolean expressions\index{Ltac!guard}\index{guard!in Ltac}} +\subsubsection[Testing boolean expressions]{Testing boolean expressions\index{Ltac!guard@\texttt{guard}}\index{guard@\texttt{guard}!in Ltac}} The {\tt guard} tactic tests a boolean expression, and fails if the expression evaluates to false. If the expression evaluates to true, it succeeds without affecting the proof. diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index df40661694..11954ed0ea 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -878,7 +878,7 @@ 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}. -\subsection[The {\tt type\_scope} interpretation scope]{The {\tt type\_scope} interpretation scope\index{type\_scope}} +\subsection[The {\tt type\_scope} interpretation scope]{The {\tt type\_scope} interpretation scope\index{type\_scope@\texttt{type\_scope}}} The scope {\tt type\_scope} has a special status. It is a primitive interpretation scope which is temporarily activated each time a diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 07d711424e..48e2df19dc 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -3,7 +3,7 @@ The distribution provides utilities to simplify some tedious works beside proof development, tactics writing or documentation. -\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\index{Coqmktop@{\tt coqmktop}}} +\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\ttindex{coqmktop}} The native-code version of \Coq\ cannot dynamically load user tactics using {\ocaml} code. It is possible to build a toplevel of \Coq, @@ -52,7 +52,7 @@ arguments. Such a wrapper can be found in the \texttt{dev/} subdirectory of the sources. \section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies} - \index{Coqdep@{\tt coqdep}}} + \ttindex{coqdep}} In order to compute modules dependencies (so to use {\tt make}), \Coq\ comes with an appropriate tool, {\tt coqdep}. @@ -75,8 +75,8 @@ See the man page of {\tt coqdep} for more details and options. \section[Creating a {\tt Makefile} for \Coq\ modules]{Creating a {\tt Makefile} for \Coq\ modules\label{Makefile} -\index{Makefile@{\tt Makefile}} -\index{CoqMakefile@{\tt coq\_Makefile}}} +\ttindex{Makefile} +\ttindex{coq\_Makefile}} \paragraph{\_CoqProject} When a proof development becomes a larger project, split into several @@ -128,8 +128,8 @@ will recursively call this target in all the subdirectories. dependencies on already defined rules. For example the following skeleton appends something to the \texttt{install} rule: \begin{quotation} -\texttt{-extra-phony ``install'' ``install-my-stuff'' ``'' - -extra-phony ``install-my-stuff'' ``'' ``something''} +\texttt{-extra-phony "install" "install-my-stuff" "" + -extra-phony "install-my-stuff" "" "something"} \end{quotation} \end{itemize} @@ -146,12 +146,12 @@ to generate a \texttt{Makefile} the first time. \texttt{Makefile} will be automatically regenerated when \texttt{\_CoqProject} is updated afterward. \section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc} -\index{Coqdoc@{\sf coqdoc}}} +\ttindex{coqdoc}} \input{./coqdoc} \section[Embedded \Coq\ phrases inside \LaTeX\ documents]{Embedded \Coq\ phrases inside \LaTeX\ documents\label{Latex} - \index{Coqtex@{\tt coq-tex}}\index{Latex@{\LaTeX}}} + \ttindex{coq-tex}\index{Latex@{\LaTeX}}} When writing a documentation about a proof development, one may want to insert \Coq\ phrases inside a \LaTeX\ document, possibly together with @@ -207,7 +207,7 @@ An inferior mode to run \Coq\ under Emacs, by Marco Maggesi, is also included in the distribution, in file \texttt{coq-inferior.el}. Instructions to use it are contained in this file. -\subsection[{\ProofGeneral}]{{\ProofGeneral}\index{\ProofGeneral}} +\subsection[{\ProofGeneral}]{{\ProofGeneral}\index{Proof General@{\ProofGeneral}}} {\ProofGeneral} is a generic interface for proof assistants based on Emacs. The main idea is that the \Coq\ commands you are @@ -221,7 +221,7 @@ files. system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!. -\section[Module specification]{Module specification\label{gallina}\index{Gallina@{\tt gallina}}} +\section[Module specification]{Module specification\label{gallina}\ttindex{gallina}} Given a \Coq\ vernacular file, the {\tt gallina} filter extracts its specification (inductive types declarations, definitions, type of diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index b66cbb4367..b42480a569 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -252,8 +252,9 @@ suffix \verb!.tex!. \item[\texmacs\ output] ~\par To translate the input files to \texmacs\ format, to be used by - the \texmacs\ Coq interface - (see \url{http://www-sop.inria.fr/lemme/Philippe.Audebaud/tmcoq/}). + the \texmacs\ Coq interface. + %broken link: + %(see \url{http://www-sop.inria.fr/lemme/Philippe.Audebaud/tmcoq/}). \end{description} -- cgit v1.2.3