From eb483c067985cc9ee7daa160efdc48806eff13e8 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 28 Jul 2017 16:48:25 +0200
Subject: Fix some coq-tex errors in the reference manual.

---
 doc/refman/Extraction.tex   | 3 +++
 doc/refman/RefMan-cic.tex   | 3 +++
 doc/refman/RefMan-sch.tex   | 1 +
 doc/refman/RefMan-tacex.tex | 2 +-
 4 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index fa3d61b1cd..a8889be814 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -365,6 +365,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 96fb1eb752..7a71d69086 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 d3719bed46..23a1c9b029 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 9f4ddc8044..cb8f916f13 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}
-- 
cgit v1.2.3