Fix some broken Coq scripts in the documentation.

7 files changed, 41 insertions, 33 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 899b196350..d75c3b8a62 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -1570,7 +1570,7 @@ If you type for instance the following ``definition'':
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
-Definition max (n p : nat) := if n <= p then p else n.
+Fail Definition max (n p : nat) := if n <= p then p else n.
 \end{coq_example}
 
 As \Coq~ says, the term ``~\texttt{n <= p}~'' is a proposition, i.e. a
@@ -1738,7 +1738,7 @@ mergesort} as an example).
 the arguments of the loop.
 
 \begin{coq_eval}
-Open Scope R_scope.
+Reset Initial.
 Require Import List.
 \end{coq_eval}
 
@@ -1751,21 +1751,25 @@ Definition R (a b:list nat) := length a < length b.
 \begin{coq_example*}
 Lemma Rwf : well_founded R.
 \end{coq_example*}
+\begin{coq_eval}
+Admitted.
+\end{coq_eval}
 
 \item Define the step function (which needs proofs that recursive
 calls are on smaller arguments).
 
-\begin{verbatim}
-Definition split (l : list nat) 
-   : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l}
-   := (* ... *) .
-Definition concat (l1 l2 : list nat) : list nat := (* ... *) .
+\begin{coq_example*}
+Definition split (l : list nat)
+   : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l}.
+Admitted.
+Definition concat (l1 l2 : list nat) : list nat.
+Admitted.
 Definition merge_step (l : list nat) (f: forall l':list nat, R l' l -> list nat) :=
   let (lH1,lH2) := (split l) in
   let (l1,H1) := lH1 in
   let (l2,H2) := lH2 in
   concat (f l1 H1) (f l2 H2).
-\end{verbatim}
+\end{coq_example*}
 
 \item Define the recursive function by fixpoint on the step function.
 
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex
index 4a4fab1538..551f6c205b 100644
--- a/doc/refman/Micromega.tex
+++ b/doc/refman/Micromega.tex
@@ -140,12 +140,12 @@ Rougthly speaking, the deductive power of {\tt lia} is the combined deductive po
 However, it solves linear goals that {\tt omega} and {\tt romega} do not solve, such as the
 following so-called \emph{omega nightmare}~\cite{TheOmegaPaper}.
 \begin{coq_example*}
-  Goal forall x y, 
-       27 <= 11 * x + 13 * y <= 45 -> 
-       -10 <= 7 * x - 9 * y <= 4 ->   False.
+Goal forall x y,
+  27 <= 11 * x + 13 * y <= 45 ->
+  -10 <= 7 * x - 9 * y <= 4 ->  False.
 \end{coq_example*}
 \begin{coq_eval}
-intro x; lia.
+intros x y; lia.
 \end{coq_eval}
 The estimation of the relative efficiency of lia \emph{vs} {\tt omega}
 and {\tt romega} is under evaluation.
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 76bcaaae67..8e078e9814 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -42,20 +42,20 @@ operation (see Section~\ref{Caseexpr}).
   generalized by the corresponding equality. As an example,
   the expression: 
 
-\begin{coq_example*}
+\begin{verbatim}
   match x with
   | 0 => t
   | S n => u
   end.
-\end{coq_example*}
+\end{verbatim}
 will be first rewritten to:
-\begin{coq_example*}
+\begin{verbatim}
   (match x as y return (x = y -> _) with
   | 0 => fun H : x = 0 -> t
   | S n => fun H : x = S n -> u
   end) (eq_refl n).
-\end{coq_example*}
-  
+\end{verbatim}
+
   This permits to get the proper equalities in the context of proof
   obligations inside clauses, without which reasoning is very limited.
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index d63d22a71c..d21c91201d 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -749,9 +749,12 @@ Function plus (n m : nat) {struct n} : nat :=
 each branch.  
 
 Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of \ident{wrong} into the body of \ident{wrong}~:
+\begin{coq_eval}
+Require List.
+\end{coq_eval}
 \begin{coq_example*}
-  Function wrong (C:nat) : nat := 
-    List.hd(List.map wrong (C::nil)).
+Fail Function wrong (C:nat) : nat :=
+  List.hd 0 (List.map wrong (C::nil)).
 \end{coq_example*}
 
 For now dependent cases are not treated for non structurally terminating functions.
@@ -1633,13 +1636,11 @@ one of the other arguments, then only the type of the first of these
 arguments is taken into account, and not an upper type of all of
 them.  As a consequence, the inference of the implicit argument of
 ``='' fails in
-
 \begin{coq_example*}
-Check nat = Prop.
+Fail Check nat = Prop.
 \end{coq_example*}
 
-but succeeds in 
-
+but succeeds in
 \begin{coq_example*}
 Check Prop = nat.
 \end{coq_example*}
@@ -2010,7 +2011,7 @@ binding as well as those introduced by tactic binding. The expression {\expr}
 can be any tactic expression as described at section~\ref{TacticLanguage}.
 
 \begin{coq_example*}
-Definition foo (x : A) : A := $( exact x )$.
+Definition foo (x : nat) : nat := $( exact x )$.
 \end{coq_example*}
 
 This construction is useful when one wants to define complicated terms using
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index cf83d0c722..9b527053c3 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -587,6 +587,9 @@ is a variable, the {\tt as} clause can be omitted and the term being
 matched can serve itself as binding name in the return type. For
 instance, the following alternative definition is accepted and has the
 same meaning as the previous one.
+\begin{coq_eval}
+Reset bool_case.
+\end{coq_eval}
 \begin{coq_example*}
 Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false)
 := match b return or (eq bool b true) (eq bool b false) with
@@ -623,7 +626,7 @@ For instance, in the following example:
 \begin{coq_example*}
 Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x :=
   match H in eq _ _ z return eq A z x with
-  | eq_refl => eq_refl A x
+  | eq_refl _ _ => eq_refl A x
   end.
 \end{coq_example*}
 the type of the branch has type {\tt eq~A~x~x} because the third
@@ -1120,7 +1123,7 @@ This is an alternative definition of lists where we specify the
 arguments of the constructors rather than their full type.
 \item
 \begin{coq_example*}
-Variant sum (A B:Set) : Set := left : A->sum A B | right : B->Sum A B.
+Variant sum (A B:Set) : Set := left : A -> sum A B | right : B -> sum A B.
 \end{coq_example*}
 The {\tt Variant} keyword is identical to the {\tt Inductive} keyword,
 except that it disallows recursive definition of types (in particular
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 8f9ba1ec60..cc262708ab 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3129,7 +3129,7 @@ follows: \comindex{Arguments}
 A constant can be marked to be never unfolded by \texttt{cbn} or
 \texttt{simpl}:
 \begin{coq_example*}
-Arguments minus x y : simpl never.
+Arguments minus n m : simpl never.
 \end{coq_example*}
 After that command an expression like \texttt{(minus (S x) y)} is left
 untouched by the tactics \texttt{cbn} and \texttt{simpl}.
@@ -3156,7 +3156,7 @@ A constant can be marked to be unfolded only if an entire set of arguments
 evaluates to a constructor. The {\tt !} symbol can be used to mark such
 arguments.
 \begin{coq_example*}
-Arguments minus !x !y.
+Arguments minus !n !m.
 \end{coq_example*}
 After that command, the expression {\tt (minus (S x) y)} is left untouched by
 {\tt simpl}, while {\tt (minus (S x) (S y))} is reduced to {\tt (minus x y)}.
@@ -3164,7 +3164,7 @@ After that command, the expression {\tt (minus (S x) y)} is left untouched by
 A special heuristic to determine if a constant has to be unfolded can be
 activated with the following command:
 \begin{coq_example*}
-Arguments minus x y : simpl nomatch.
+Arguments minus n m : simpl nomatch.
 \end{coq_example*}
 The heuristic avoids to perform a simplification step that would
 expose a {\tt match} construct in head position. For example the
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 3770ba574b..2c9602a229 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -658,17 +658,17 @@ arguments (or whatever subrelation of the pointwise extension).
 For example, one could declare the \texttt{map} combinator on lists as 
 a morphism:
 \begin{coq_eval}
-Require Import List.
+Require Import List Setoid Morphisms.
 Set Implicit Arguments.
 Inductive list_equiv {A:Type} (eqA : relation A) : relation (list A) :=
 | eq_nil : list_equiv eqA nil nil
-| eq_cons : forall x y, eqA x y -> 
+| eq_cons : forall x y, eqA x y ->
   forall l l', list_equiv eqA l l' -> list_equiv eqA (x :: l) (y :: l').
+Generalizable All Variables.
 \end{coq_eval}
 \begin{coq_example*}
 Instance map_morphism `{Equivalence A eqA, Equivalence B eqB} :
-  Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) 
-     (@map A B).
+  Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B).
 \end{coq_example*}
 
 where \texttt{list\_equiv} implements an equivalence on lists