Fix some broken Coq scripts in the reference manual.

6 files changed, 13 insertions, 13 deletions

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