Merge PR #934: Fix some coq-tex errors in the reference manual.

4 files changed, 8 insertions, 1 deletions

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 8cb049d50..499239b6f 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -381,6 +381,9 @@ some specific {\tt Extract Constant} when primitive counterparts exist.
 
 \Example
 Typical examples are the following:
+\begin{coq_eval}
+Require Extraction.
+\end{coq_eval}
 \begin{coq_example}
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 96fb1eb75..7a71d6908 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1425,6 +1425,9 @@ If there is an hypothesis $h:a=b$ in the local context, it can be used for
 rewriting not only in logical propositions but also in any type.
 % In that case, the term \verb!eq_rec! which was defined as an axiom, is
 % now a term of the calculus.
+\begin{coq_eval}
+Require Extraction.
+\end{coq_eval}
 \begin{coq_example}
 Print eq_rec.
 Extraction eq_rec.
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index d3719bed4..23a1c9b02 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -227,6 +227,7 @@ We define the function \texttt{div2} as follows:
 
 \begin{coq_eval}
 Reset Initial.
+Require Import FunInd.
 \end{coq_eval}
 
 \begin{coq_example*}
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 9f4ddc804..cb8f916f1 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -849,7 +849,7 @@ Ltac DSimplif trm :=
 Ltac Length trm :=
   match trm with
   | (_ * ?B) => let succ := Length B in constr:(S succ)
-  | _ => constr:1
+  | _ => constr:(1)
   end.
 Ltac assoc := repeat rewrite <- Ass.
 \end{coq_example}