aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile.doc42
-rw-r--r--doc/RecTutorial/RecTutorial.tex49
-rw-r--r--doc/refman/RefMan-ext.tex6
-rw-r--r--doc/refman/RefMan-gal.tex6
-rw-r--r--doc/refman/RefMan-lib.tex18
-rw-r--r--doc/refman/RefMan-ltac.tex51
-rwxr-xr-xdoc/tutorial/Tutorial.tex41
-rw-r--r--lib/pp_control.ml4
-rw-r--r--theories/Logic/Hurkens.v2
9 files changed, 131 insertions, 88 deletions
diff --git a/Makefile.doc b/Makefile.doc
index 5afd12393..9382e1b6f 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -17,15 +17,15 @@ doc: refman faq tutorial rectutorial stdlib ide/index_urls.txt
doc-html:\
doc/tutorial/Tutorial.v.html doc/refman/html/index.html \
- doc/faq/html/index.html doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.v.html
+ doc/faq/html/index.html doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.html
doc-pdf:\
doc/tutorial/Tutorial.v.pdf doc/refman/Reference-Manual.pdf \
- doc/faq/FAQ.v.pdf doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.v.pdf
+ doc/faq/FAQ.v.pdf doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.pdf
doc-ps:\
doc/tutorial/Tutorial.v.ps doc/refman/Reference-Manual.ps \
- doc/faq/FAQ.v.ps doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.v.ps
+ doc/faq/FAQ.v.ps doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.ps
refman: \
doc/refman/html/index.html doc/refman/Reference-Manual.ps doc/refman/Reference-Manual.pdf
@@ -38,8 +38,8 @@ stdlib: \
faq: doc/faq/html/index.html doc/faq/FAQ.v.ps doc/faq/FAQ.v.pdf
-rectutorial: doc/RecTutorial/RecTutorial.v.html \
- doc/RecTutorial/RecTutorial.v.ps doc/RecTutorial/RecTutorial.v.pdf
+rectutorial: doc/RecTutorial/RecTutorial.html \
+ doc/RecTutorial/RecTutorial.ps doc/RecTutorial/RecTutorial.pdf
######################################################################
### Implicit rules
@@ -216,32 +216,32 @@ doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Li
(cd doc/stdlib;\
$(LATEX) -interaction=batchmode Library;\
$(LATEX) -interaction=batchmode Library > /dev/null;\
- ../tools/show_latex_messages Library.log)
+ ../tools/show_latex_messages -no-overfull Library.log)
doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.dvi
(cd doc/stdlib;\
$(PDFLATEX) -interaction=batchmode Library;\
- ../tools/show_latex_messages Library.log)
+ ../tools/show_latex_messages -no-overfull Library.log)
######################################################################
# Tutorial on inductive types
######################################################################
-doc/RecTutorial/RecTutorial.v.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.tex
+doc/RecTutorial/RecTutorial.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.tex
(cd doc/RecTutorial;\
- $(LATEX) -interaction=batchmode RecTutorial.v;\
- $(BIBTEX) -terse RecTutorial.v;\
- $(LATEX) -interaction=batchmode RecTutorial.v > /dev/null;\
- $(LATEX) -interaction=batchmode RecTutorial.v > /dev/null;\
- ../tools/show_latex_messages RecTutorial.v.log)
+ $(LATEX) -interaction=batchmode RecTutorial;\
+ $(BIBTEX) -terse RecTutorial;\
+ $(LATEX) -interaction=batchmode RecTutorial > /dev/null;\
+ $(LATEX) -interaction=batchmode RecTutorial > /dev/null;\
+ ../tools/show_latex_messages RecTutorial.log)
-doc/RecTutorial/RecTutorial.v.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.dvi
+doc/RecTutorial/RecTutorial.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.dvi
(cd doc/RecTutorial;\
- $(PDFLATEX) -interaction=batchmode RecTutorial.v.tex;\
- ../tools/show_latex_messages RecTutorial.v.log)
+ $(PDFLATEX) -interaction=batchmode RecTutorial.tex;\
+ ../tools/show_latex_messages RecTutorial.log)
-doc/RecTutorial/RecTutorial.v.html: doc/RecTutorial/RecTutorial.v.tex
- (cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial.v)
+doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex
+ (cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial)
######################################################################
# Index file for CoqIDE
@@ -267,7 +267,7 @@ install-doc-html:
$(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib faq)
$(INSTALLLIB) doc/refman/html/* $(FULLDOCDIR)/html/refman
$(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib
- $(INSTALLLIB) doc/RecTutorial/RecTutorial.v.html $(FULLDOCDIR)/html/RecTutorial.html
+ $(INSTALLLIB) doc/RecTutorial/RecTutorial.html $(FULLDOCDIR)/html/RecTutorial.html
$(INSTALLLIB) doc/faq/html/* $(FULLDOCDIR)/html/faq
$(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html
@@ -278,8 +278,8 @@ install-doc-printable:
$(INSTALLLIB) doc/refman/Reference-Manual.ps \
doc/stdlib/Library.ps $(FULLDOCDIR)/ps
$(INSTALLLIB) doc/tutorial/Tutorial.v.pdf $(FULLDOCDIR)/pdf/Tutorial.pdf
- $(INSTALLLIB) doc/RecTutorial/RecTutorial.v.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf
+ $(INSTALLLIB) doc/RecTutorial/RecTutorial.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf
$(INSTALLLIB) doc/faq/FAQ.v.pdf $(FULLDOCDIR)/pdf/FAQ.pdf
$(INSTALLLIB) doc/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps
- $(INSTALLLIB) doc/RecTutorial/RecTutorial.v.ps $(FULLDOCDIR)/ps/RecTutorial.ps
+ $(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps
$(INSTALLLIB) doc/faq/FAQ.v.ps $(FULLDOCDIR)/ps/FAQ.ps
diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex
index 79b4f7f1a..372f13326 100644
--- a/doc/RecTutorial/RecTutorial.tex
+++ b/doc/RecTutorial/RecTutorial.tex
@@ -724,7 +724,7 @@ for \linebreak ``~\citecoq{ex (fun $x$:$A$ \funarrow{} $B$)}~''.
\noindent The former quantifier inhabits the universe of propositions.
As for the conjunction and disjunction connectives, there is also another
version of existential quantification inhabiting the universes $\Type_i$,
-which is noted \texttt{sig $P$}. The syntax
+which is written \texttt{sig $P$}. The syntax
``~\citecoq{\{$x$:$A$ | $B$\}}~'' is an abreviation for ``~\citecoq{sig (fun $x$:$A$ {\funarrow} $B$)}~''.
@@ -934,7 +934,7 @@ Definition predecessor : {\prodsym} n:nat, pred_spec n.
Defined.
\end{alltt}
-If we print the term built by {\coq}, we can observe its dependent pattern-matching structure:
+If we print the term built by {\coq}, its dependent pattern-matching structure can be observed:
\begin{alltt}
predecessor = fun n : nat {\funarrow}
@@ -950,8 +950,9 @@ predecessor = fun n : nat {\funarrow}
\end{alltt}
-Notice that there are many variants to the pattern ``~\texttt{intros \dots; case \dots}~''. Look at the reference manual and/or the book: tactics
-\texttt{destruct}, ``~\texttt{intro \emph{pattern}}~'', etc.
+Notice that there are many variants to the pattern ``~\texttt{intros \dots; case \dots}~''. Look at for tactics
+``~\texttt{destruct}~'', ``~\texttt{intro \emph{pattern}}~'', etc. in
+the reference manual and/or the book.
\noindent The command \texttt{Extraction} \refmancite{Section
\ref{ExtractionIdent}} can be used to see the computational
@@ -1240,7 +1241,7 @@ Let $n$ and $p$ be terms of type \citecoq{nat}, and $Q$ a predicate
of type $\citecoq{nat}\arrow{}\Prop$.
If $H$ is a proof of ``~\texttt{n {\coqle} p}~'',
$H_0$ a proof of ``~\texttt{$Q$ n}~'' and
-$H_S$ a proof of ``~\citecoq{{\prodsym}m:nat, n {\coqle} m {\arrow} Q (S m)}~'',
+$H_S$ a proof of the statement ``~\citecoq{{\prodsym}m:nat, n {\coqle} m {\arrow} Q (S m)}~'',
then the term
\begin{alltt}
match H in (_ {\coqle} q) return (Q q) with
@@ -2604,8 +2605,8 @@ End Principle_of_Double_Induction.
\end{alltt}
Changing the type of $P$ into $\nat\rightarrow\nat\rightarrow\Type$,
-another combinator \texttt{nat\_double\_rect} for constructing
-(certified) programs can be defined in exactly the same way.
+another combinator for constructing
+(certified) programs, \texttt{nat\_double\_rect}, can be defined in exactly the same way.
This definition is left as an exercise.\label{natdoublerect}
\iffalse
@@ -2751,8 +2752,8 @@ has a universally quantified formula as conclusion, which confuses
Therefore,
-in this case the abstraction must be explicited using the tactic
-\texttt{pattern}. Once the right abstraction is provided, the rest of
+in this case the abstraction must be explicited using the
+\texttt{pattern} tactic. Once the right abstraction is provided, the rest of
the proof is immediate:
\begin{alltt}
@@ -2804,8 +2805,8 @@ Defined.
\begin{exercise}
\begin{enumerate}
-\item Define a recursive function \emph{nat2itree}
-mapping any natural number $n$ into an infinitely branching
+\item Define a recursive function of name \emph{nat2itree}
+that maps any natural number $n$ into an infinitely branching
tree of height $n$.
\item Provide an elimination combinator for these trees.
\item Prove that the relation \citecoq{itree\_le} is a preorder
@@ -2831,7 +2832,7 @@ for all n and p. (\citecoq{le'} is defined in section \ref{parameterstuff}).
Structural induction is a strong elimination rule for inductive types.
This method can be used to define any function whose termination is
-based on the well-foundedness of certain order relation $R$ decreasing
+a consequence of the well-foundedness of a certain order relation $R$ decreasing
at each recursive call. What makes this principle so strong is the
possibility of reasoning by structural induction on the proof that
certain $R$ is well-founded. In order to illustrate this we have
@@ -2867,8 +2868,8 @@ let rec div x y =
\end{verbatim}
-The equality test on natural numbers can be represented as the
-function \textsl{eq\_nat\_dec} defined page \pageref{iseqpage}. Giving $x$ and
+The equality test on natural numbers can be implemented using the
+function \textsl{eq\_nat\_dec} that is defined page \pageref{iseqpage}. Giving $x$ and
$y$, this function yields either the value $(\textsl{left}\;p)$ if
there exists a proof $p:x=y$, or the value $(\textsl{right}\;q)$ if
there exists $q:a\not = b$. The subtraction function is already
@@ -3112,7 +3113,7 @@ The term "Vnil A" has type "vector A 0" while it is expected to have type
"vector A n"
\end{alltt}
-In effect, the equality ``~\citecoq{v = Vnil A}~'' is ill typed,
+In effect, the equality ``~\citecoq{v = Vnil A}~'' is ill-typed and this is
because the type ``~\citecoq{vector A n}~'' is not \emph{convertible}
with ``~\citecoq{vector A 0}~''.
@@ -3264,11 +3265,11 @@ on vectors of same length:
\begin{alltt}
Definition vector_double_rect :
- {\prodsym} (A:Type) (P: {\prodsym} (n:nat),(vector A n){\arrow}(vector A n) {\arrow} Type),
- P 0 Vnil Vnil {\arrow}
- ({\prodsym} n (v1 v2 : vector A n) a b, P n v1 v2 {\arrow}
- P (S n) (Vcons a v1) (Vcons b v2)) {\arrow}
- {\prodsym} n (v1 v2 : vector A n), P n v1 v2.
+ {\prodsym} (A:Type) (P: {\prodsym} (n:nat),(vector A n){\arrow}(vector A n) {\arrow} Type),
+ P 0 Vnil Vnil {\arrow}
+ ({\prodsym} n (v1 v2 : vector A n) a b, P n v1 v2 {\arrow}
+ P (S n) (Vcons a v1) (Vcons b v2)) {\arrow}
+ {\prodsym} n (v1 v2 : vector A n), P n v1 v2.
induction n.
intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
auto.
@@ -3361,7 +3362,7 @@ CoInductive LList (A: Type) : Type :=
It is also possible to define co-inductive types for the
-trees with infinite branches (see Chapter 13 of~\cite{coqart}).
+trees with infinitely-many branches (see Chapter 13 of~\cite{coqart}).
Structural induction is the way of expressing that inductive types
only contain well-founded objects. Hence, this elimination principle
@@ -3555,7 +3556,7 @@ Qed.
\end{alltt}
\begin{exercise}
-Define a co-inductive type $Nat$ containing non-standard
+Define a co-inductive type of name $Nat$ that contains non-standard
natural numbers --this is, verifying
$$\exists m \in \mbox{\texttt{Nat}}, \forall\, n \in \mbox{\texttt{Nat}}, n<m$$.
@@ -3591,8 +3592,8 @@ Proof.
Qed.
Lemma injection_demo : {\prodsym} (A:Type)(a b : A)(l l': LList A),
- LCons a (LCons b l) = LCons b (LCons a l') {\arrow}
- a = b {\coqand} l = l'.
+ LCons a (LCons b l) = LCons b (LCons a l') {\arrow}
+ a = b {\coqand} l = l'.
Proof.
intros A a b l l' e; injection e; auto.
Qed.
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 8b404f4ef..501f9b0b1 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -343,7 +343,7 @@ for all the arguments. For example, the preceding example can be written:
Reset fst.
\end{coq_eval}
\begin{coq_example}
-Definition fst (A B:Set) (p:A * B) := let 'pair x _ := p in x.
+Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x.
\end{coq_example}
This is useful to match deeper inside tuples and also to use notations
@@ -351,10 +351,10 @@ for the pattern, as the syntax {\tt let 'p := t in b} allows arbitrary
patterns to do the deconstruction. For example:
\begin{coq_example}
-Definition deep_tuple (A : Set) (x : (A * A) * (A * A)) : A * A * A * A :=
+Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A :=
let '((a,b), (c, d)) := x in (a,b,c,d).
Notation " x 'with' p " := (exist _ x p) (at level 20).
-Definition proj1_sig' (A :Set) (P : A -> Prop) (t:{ x : A | P x }) : A :=
+Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A :=
let 'x with p := t in x.
\end{coq_example}
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 3a4d7f03e..48c18e265 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -226,7 +226,7 @@ Chapter \ref{Addoc-syntax}.
\begin{figure}[htbp]
\begin{centerframe}
-\begin{tabular}{lcl@{\qquad}r}
+\begin{tabular}{lcl@{\quad~}r} % warning: page width exceeded with \qquad
{\term} & ::= &
{\tt forall} {\binderlist} {\tt ,} {\term} &(\ref{products})\\
& $|$ & {\tt fun} {\binderlist} {\tt =>} {\term} &(\ref{abstractions})\\
@@ -266,10 +266,10 @@ Chapter \ref{Addoc-syntax}.
{\binderlist} & ::= & \nelist{\name}{} {\typecstr} & \ref{Binders} \\
& $|$ & {\binder} \nelist{\binderlet}{} &\\
&&&\\
-{\binder} & ::= & {\name} & \ref{Binders} \\
+{\binder} & ::= & {\name} & (\ref{Binders}) \\
& $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\
&&&\\
-{\binderlet} & ::= & {\binder} & \ref{Binders} \\
+{\binderlet} & ::= & {\binder} & (\ref{Binders}) \\
& $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\
& & &\\
{\name} & ::= & {\ident} &\\
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index d15859047..24eb3d112 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -267,11 +267,11 @@ Abort.
\begin{coq_example*}
End equality.
Definition eq_ind_r :
- forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
+ forall (A:Type) (x:A) (P:A->Prop), P x -> forall y:A, y = x -> P y.
Definition eq_rec_r :
- forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
+ forall (A:Type) (x:A) (P:A->Set), P x -> forall y:A, y = x -> P y.
Definition eq_rect_r :
- forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
+ forall (A:Type) (x:A) (P:A->Type), P x -> forall y:A, y = x -> P y.
\end{coq_example*}
\begin{coq_eval}
Abort.
@@ -290,8 +290,9 @@ arguments. The theorem are names {\tt f\_equal2}, {\tt f\_equal3},
For instance {\tt f\_equal3} is defined the following way.
\begin{coq_example*}
Theorem f_equal3 :
- forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2)
- (x3 y3:A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
+ forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B)
+ (x1 y1:A1) (x2 y2:A2) (x3 y3:A3),
+ x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
\end{coq_example*}
\begin{coq_eval}
Abort.
@@ -478,7 +479,9 @@ in the \verb"Set" \verb"A+{B}".
\ttindex{A+\{B\}}
\begin{coq_example*}
-Inductive sumor (A:Set) (B:Prop) : Set := inleft (_:A) | inright (_:B).
+Inductive sumor (A:Set) (B:Prop) : Set :=
+| inleft (_:A)
+| inright (_:B).
\end{coq_example*}
We may define variants of the axiom of choice, like in Martin-Löf's
@@ -675,7 +678,8 @@ induction principle.
\begin{coq_example*}
Theorem nat_case :
- forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.
+ forall (n:nat) (P:nat -> Prop),
+ P 0 -> (forall m:nat, P (S m)) -> P n.
\end{coq_example*}
\begin{coq_eval}
Abort All.
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index d5c6dbfdb..5b447f350 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -22,7 +22,7 @@ problems.
\def\letclause{\textrm{\textsl{let\_clause}}}
\def\matchrule{\textrm{\textsl{match\_rule}}}
\def\contextrule{\textrm{\textsl{context\_rule}}}
-\def\contexthyps{\textrm{\textsl{context\_hyps}}}
+\def\contexthyp{\textrm{\textsl{context\_hyp}}}
\def\tacarg{\nterm{tacarg}}
\def\cpattern{\nterm{cpattern}}
@@ -166,11 +166,12 @@ is understood as
\letclause & ::= & {\ident} \sequence{\name}{} {\tt :=} {\tacexpr}\\
\\
\contextrule & ::= &
- \nelist{\contexthyps}{\tt ,} {\tt |-}{\cpattern} {\tt =>} {\tacexpr}\\
+ \nelist{\contexthyp}{\tt ,} {\tt |-}{\cpattern} {\tt =>} {\tacexpr}\\
& $|$ & {\tt |-} {\cpattern} {\tt =>} {\tacexpr}\\
& $|$ & {\tt \_ =>} {\tacexpr}\\
\\
-\contexthyps & ::= & {\name} {\tt :} {\cpattern}\\
+\contexthyp & ::= & {\name} {\tt :} {\cpattern}\\
+ & $|$ & {\name} {\tt :=} {\cpattern} \zeroone{{\tt :} {\cpattern}}\\
\\
\matchrule & ::= &
{\cpattern} {\tt =>} {\tacexpr}\\
@@ -268,31 +269,53 @@ A sequence is an expression of the following form:
\begin{quote}
{\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$
\end{quote}
-{\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
-$v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is then applied
-and $v_2$ is applied to every subgoal generated by the application of
-$v_1$. Sequence is left-associative.
+The expressions {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated
+to $v_1$ and $v_2$ which have to be tactic values. The tactic $v_1$ is
+then applied and $v_2$ is applied to every subgoal generated by the
+application of $v_1$. Sequence is left-associative.
\subsubsection[General sequence]{General sequence\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}}
%\tacindex{; [ | ]}
%\index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}}
\index{Tacticals!; [ \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
-We can generalize the previous sequence operator as
+A general sequence has the following form:
\begin{quote}
{\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
{\tacexpr}$_n$ {\tt ]}
\end{quote}
-{\tacexpr}$_i$ is evaluated to $v_i$, for $i=0,...,n$. $v_0$ is
-applied and $v_i$ is applied to the $i$-th generated subgoal by the
-application of $v_0$, for $=1,...,n$. It fails if the application of
-$v_0$ does not generate exactly $n$ subgoals.
+The expressions {\tacexpr}$_i$ are evaluated to $v_i$, for $i=0,...,n$
+and all have to be tactics. The tactic $v_0$ is applied and $v_i$ is
+applied to the $i$-th generated subgoal by the application of $v_0$,
+for $=1,...,n$. It fails if the application of $v_0$ does not generate
+exactly $n$ subgoals.
-\variant If no tactic is given for the $i$-th generated subgoal, it
+\begin{Variants}
+ \item If no tactic is given for the $i$-th generated subgoal, it
behaves as if the tactic {\tt idtac} were given. For instance, {\tt
split ; [ | auto ]} is a shortcut for
{\tt split ; [ idtac | auto ]}.
+ \item {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
+ {\tacexpr}$_i$ {\tt |} {\tt ..} {\tt |} {\tacexpr}$_{i+1+j}$ {\tt |}
+ $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
+
+ In this variant, {\tt idtac} is used for the subgoals numbered from
+ $i+1$ to $i+j$ (assuming $n$ is the number of subgoals).
+
+ Note that {\tt ..} is part of the syntax, while $...$ is the meta-symbol used
+ to describe a list of {\tacexpr} of arbitrary length.
+
+ \item {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
+ {\tacexpr}$_i$ {\tt |} {\tacexpr} {\tt ..} {\tt |}
+ {\tacexpr}$_{i+1+j}$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
+
+ In this variant, {\tacexpr} is used instead of {\tt idtac} for the
+ subgoals numbered from $i+1$ to $i+j$.
+
+\end{Variants}
+
+
\subsubsection[For loop]{For loop\tacindex{do}
\index{Tacticals!do@{\tt do}}}
@@ -591,7 +614,7 @@ We can make pattern matching on goals using the following expression:
\end{quote}
If each hypothesis pattern $hyp_{1,i}$, with $i=1,...,m_1$
-is matched (non-linear first order unification) by an hypothesis of
+is matched (non-linear first-order unification) by an hypothesis of
the goal and if {\cpattern}$_1$ is matched by the conclusion of the
goal, then {\tacexpr}$_1$ is evaluated to $v_1$ by substituting the
pattern matching to the metavariables and the real hypothesis names
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 8944ec979..219706e35 100755
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -108,6 +108,10 @@ $e:\tau(E)$ for the judgment that $e$ is of type $E$.
You may request \Coq~ to return to you the type of a valid expression by using
the command \verb:Check::
+\begin{coq_eval}
+Set Printing Width 60.
+\end{coq_eval}
+
\begin{coq_example}
Check O.
\end{coq_example}
@@ -169,9 +173,9 @@ arrow function constructor, in order to get a functional type
\begin{coq_example}
Check (nat -> Prop).
\end{coq_example}
-which may be composed again with \verb:nat: in order to obtain the
+which may be composed one more times with \verb:nat: in order to obtain the
type \verb:nat->nat->Prop: of binary relations over natural numbers.
-Actually \verb:nat->nat->Prop: is an abbreviation for
+Actually the type \verb:nat->nat->Prop: is an abbreviation for
\verb:nat->(nat->Prop):.
Functional notions may be composed in the usual way. An expression $f$
@@ -213,7 +217,7 @@ argument \verb:m: of type \verb:nat: in order to build its result as
\begin{coq_example}
Definition double (m:nat) := plus m m.
\end{coq_example}
-This definition introduces the constant \texttt{double} defined as the
+This introduces the constant \texttt{double} defined as the
expression \texttt{fun m:nat => plus m m}.
The abstraction introduced by \texttt{fun} is explained as follows. The expression
\verb+fun x:A => e+ is well formed of type \verb+A->B+ in a context
@@ -445,7 +449,6 @@ conjunctive goal into the two subgoals:
\begin{coq_example}
split.
\end{coq_example}
-
and the proof is now trivial. Indeed, the whole proof is obtainable as follows:
\begin{coq_example}
Restart.
@@ -540,7 +543,7 @@ explanations. The \texttt{fun} prefix, such as \verb+fun H:A\/B =>+,
corresponds
to \verb:intro H:, whereas a subterm such as
\verb:(or_intror: \verb:B H0):
-corresponds to the sequence \verb:apply or_intror; exact H0:.
+corresponds to the sequence of tactics \verb:apply or_intror; exact H0:.
The generic combinator \verb:or_intror: needs to be instantiated by
the two properties \verb:B: and \verb:A:. Because \verb:A: can be
deduced from the type of \verb:H0:, only \verb:B: is printed.
@@ -559,7 +562,7 @@ Qed.
\subsection{Classical reasoning}
-\verb:tauto: always comes back with an answer. Here is an example where it
+The tactic \verb:tauto: always comes back with an answer. Here is an example where it
fails:
\begin{coq_example}
Lemma Peirce : ((A -> B) -> A) -> A.
@@ -661,6 +664,9 @@ remove a section, or we may return to the initial state using~:
\begin{coq_example}
Reset Initial.
\end{coq_example}
+\begin{coq_eval}
+Set Printing Width 60.
+\end{coq_eval}
We shall now declare a new \verb:Section:, which will allow us to define
notions local to a well-delimited scope. We start by assuming a domain of
@@ -705,7 +711,7 @@ predicate as argument:
Check ex.
\end{coq_example}
and the notation \verb+(exists x:D, P x)+ is just concrete syntax for
-\verb+(ex D (fun x:D => P x))+.
+the expression \verb+(ex D (fun x:D => P x))+.
Existential quantification is handled in \Coq~ in a similar
fashion to the connectives \verb:/\: and \verb:\/: : it is introduced by
the proof combinator \verb:ex_intro:, which is invoked by the specific
@@ -842,7 +848,8 @@ elim (EM (exists x, ~ P x)).
We first look at the first case. Let Tom be the non-drinker:
\begin{coq_example}
-intro Non_drinker; elim Non_drinker; intros Tom Tom_does_not_drink.
+intro Non_drinker; elim Non_drinker;
+ intros Tom Tom_does_not_drink.
\end{coq_example}
We conclude in that case by considering Tom, since his drinking leads to
@@ -1026,7 +1033,8 @@ predicates over some universe \verb:U:. For instance:
Variable U : Type.
Definition set := U -> Prop.
Definition element (x:U) (S:set) := S x.
-Definition subset (A B:set) := forall x:U, element x A -> element x B.
+Definition subset (A B:set) :=
+ forall x:U, element x A -> element x B.
\end{coq_example}
Now, assume that we have loaded a module of general properties about
@@ -1151,7 +1159,7 @@ right; trivial.
\end{coq_example}
Indeed, the whole proof can be done with the combination of the
-\verb:simple induction: tactic, which combines \verb:intro: and \verb:elim:,
+ \verb:simple: \verb:induction:, which combines \verb:intro: and \verb:elim:,
with good old \verb:auto::
\begin{coq_example}
Restart.
@@ -1197,13 +1205,15 @@ an expression to its {\sl normal form}:
\begin{coq_example}
Eval cbv beta in
((fun _:nat => nat) O ->
- (forall y:nat, (fun _:nat => nat) y -> (fun _:nat => nat) (S y)) ->
+ (forall y:nat,
+ (fun _:nat => nat) y -> (fun _:nat => nat) (S y)) ->
forall n:nat, (fun _:nat => nat) n).
\end{coq_example}
Let us now show how to program addition with primitive recursion:
\begin{coq_example}
-Definition addition (n m:nat) := prim_rec m (fun p rec:nat => S rec) n.
+Definition addition (n m:nat) :=
+ prim_rec m (fun p rec:nat => S rec) n.
\end{coq_example}
That is, we specify that \verb+(addition n m)+ computes by cases on \verb:n:
@@ -1242,6 +1252,9 @@ Reset bool.
\begin{coq_eval}
Reset Initial.
\end{coq_eval}
+\begin{coq_eval}
+Set Printing Width 60.
+\end{coq_eval}
Let us now show how to do proofs by structural induction. We start with easy
properties of the \verb:plus: function we just defined. Let us first
@@ -1508,13 +1521,13 @@ development is not type-checked again.
\section{Creating your own modules}
-You may create your own modules, by writing \Coq~ commands in a file,
+You may create your own module files, by writing {\Coq} commands in a file,
say \verb:my_module.v:. Such a module may be simply loaded in the current
context, with command \verb:Load my_module:. It may also be compiled,
in ``batch'' mode, using the UNIX command
\verb:coqc:. Compiling the module \verb:my_module.v: creates a
file \verb:my_module.vo:{} that can be reloaded with command
-\verb:Require Import my_module:.
+\verb:Require: \verb:Import: \verb:my_module:.
If a required module depends on other modules then the latters are
automatically required beforehand. However their contents is not
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 67ae4a20a..7617d5ca4 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -105,5 +105,7 @@ let set_depth_boxes v =
let get_margin () = Some (Format.pp_get_margin !std_ft ())
let set_margin v =
- Format.pp_set_margin !std_ft (match v with None -> default_margin | Some v -> v)
+ let v = match v with None -> default_margin | Some v -> v in
+ Format.pp_set_margin !std_ft v;
+ Format.pp_set_margin !deep_ft v
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 46a574322..71c9af50b 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -19,7 +19,7 @@
and Applications (TLCA'95), 1995.
- [Geuvers] "Inconsistency of Classical Logic in Type Theory", 2001
- (see www.cs.kun.nl/~herman/note.ps.gz).
+ (see http://www.cs.kun.nl/~herman/note.ps.gz).
*)
Section Paradox.