aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/CanonicalStructures.tex16
-rw-r--r--doc/refman/Cases.tex49
-rw-r--r--doc/refman/Misc.tex2
-rw-r--r--doc/refman/Polynom.tex115
-rw-r--r--doc/refman/RefMan-com.tex3
-rw-r--r--doc/refman/RefMan-decl.tex81
-rw-r--r--doc/refman/RefMan-ext.tex6
-rw-r--r--doc/refman/RefMan-gal.tex2
-rw-r--r--doc/refman/RefMan-lib.tex8
-rw-r--r--doc/refman/RefMan-ltac.tex75
-rw-r--r--doc/refman/RefMan-mod.tex2
-rw-r--r--doc/refman/RefMan-oth.tex5
-rw-r--r--doc/refman/RefMan-pro.tex10
-rw-r--r--doc/refman/RefMan-syn.tex2
-rw-r--r--doc/refman/RefMan-tac.tex6
-rw-r--r--doc/refman/RefMan-tacex.tex2
-rw-r--r--doc/refman/RefMan-uti.tex20
-rw-r--r--doc/refman/coqdoc.tex5
18 files changed, 227 insertions, 182 deletions
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex
index c8e36197ca..b1c278cede 100644
--- a/doc/refman/CanonicalStructures.tex
+++ b/doc/refman/CanonicalStructures.tex
@@ -305,15 +305,21 @@ 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) := 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}
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/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/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-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-decl.tex b/doc/refman/RefMan-decl.tex
index 292b8bbed2..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.
@@ -381,7 +393,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 +506,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).
@@ -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.
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 193479cceb..3605a716e7 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.
@@ -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-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-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-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-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}
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}
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-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-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
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}
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 17:01:46 +0000