Manual fixed w.r.t. STM

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16675 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 19 insertions, 14 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index fc511a45c..f5ad9d913 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -417,9 +417,9 @@ patterns to do the deconstruction. For example:
 \begin{coq_example}
 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).
+Notation " x 'With' p " := (exist _ x p) (at level 20).
 Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A :=
-  let 'x with p := t in x.
+  let 'x With p := t in x.
 \end{coq_example}
 
 When printing definitions which are written using this construct it
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 26c564e52..da2e099f9 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -156,11 +156,13 @@ Section Projections.
 Variables A B : Prop.
 Theorem proj1 : A /\ B -> A.
 Theorem proj2 : A /\ B -> B.
-End Projections.
 \end{coq_example*}
 \begin{coq_eval}
 Abort All.
 \end{coq_eval}
+\begin{coq_example*}
+End Projections.
+\end{coq_example*}
 \ttindex{or}
 \ttindex{or\_introl}
 \ttindex{or\_intror}
@@ -384,10 +386,10 @@ Inductive prod (A B:Set) : Set := pair (_:A) (_:B).
 Section projections.
 Variables A B : Set.
 Definition fst (H: prod A B) := match H with
-                                | pair x y => x
+                                | pair _ _ x y => x
                                 end.
 Definition snd (H: prod A B) := match H with
-                                | pair x y => y
+                                | pair _ _ x y => y
                                 end.
 End projections.
 \end{coq_example*}
@@ -443,15 +445,15 @@ constructor of types in \verb:Type:.
 
 \begin{coq_example*}
 Inductive sigT (A:Type) (P:A -> Type) : Type := existT (x:A) (_:P x).
-Section Projections.
+Section Projections2.
 Variable A : Type.
 Variable P : A -> Type.
 Definition projT1 (H:sigT A P) := let (x, h) := H in x.
 Definition projT2 (H:sigT A P) :=
   match H return P (projT1 H) with
-    existT x h => h
+    existT _ _ x h => h
   end.
-End Projections.
+End Projections2.
 Inductive sigT2 (A: Type) (P Q:A -> Type) : Type :=
     existT2 (x:A) (_:P x) (_:Q x).
 \end{coq_example*}
@@ -537,7 +539,7 @@ interpretation.
 \begin{coq_example*}
 Definition except := False_rec.
 Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
-Theorem and_rect :
+Theorem and_rect2 :
  forall (A B:Prop) (P:Type), (A -> B -> P) -> A /\ B -> P.
 \end{coq_example*}
 %\begin{coq_eval}
@@ -626,7 +628,7 @@ Fixpoint plus (n m:nat) {struct n} : nat :=
   match n with
   | 0 => m
   | S p => S (p + m)
-  end.
+  end
 where "n + m" := (plus n m) : nat_scope.
 Lemma plus_n_O : forall n:nat, n = n + 0.
 Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
@@ -639,7 +641,7 @@ Fixpoint mult (n m:nat) {struct n} : nat :=
   match n with
   | 0 => 0
   | S p => m + p * m
-  end.
+  end
 where "n * m" := (mult n m) : nat_scope.
 Lemma mult_n_O : forall n:nat, 0 = n * 0.
 Lemma mult_n_Sm : forall n m:nat, n * m + n = n * (S m).
@@ -660,7 +662,7 @@ Finally, it gives the definition of the usual orderings \verb:le:,
 \begin{coq_example*}
 Inductive le (n:nat) : nat -> Prop :=
   | le_n : le n n
-  | le_S : forall m:nat, n <= m -> n <= (S m).
+  | le_S : forall m:nat, n <= m -> n <= (S m)
 where "n <= m" := (le n m) : nat_scope.
 Definition lt (n m:nat) := S n <= m.
 Definition ge (n m:nat) := m <= n.
@@ -712,7 +714,7 @@ Variable A : Type.
 Variable R : A -> A -> Prop.
 Inductive Acc (x:A) : Prop :=
     Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.
-Lemma Acc_inv : Acc x -> forall y:A, R y x -> Acc y.
+Lemma Acc_inv x : Acc x -> forall y:A, R y x -> Acc y.
 \end{coq_example*}
 \begin{coq_eval}
 destruct 1; trivial.
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 4029e4e28..5f8bd300f 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -956,6 +956,9 @@ r {\qstring}: & advance up to the next call to ``{\tt idtac} {\qstring}''\\
 \begin{figure}[b]
 \begin{center}
 \fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
 \begin{coq_example*}
 Require Import List.
 Section Sort.
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a091da2df..805b2cee0 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -882,7 +882,7 @@ Qed.
 Goal forall n:nat, n = 0 -> n = 0.
 intros [ | ] H.
 Show 2.
-Undo.
+Undo 2.
 intros [ | ]; intros H.
 Show 2.
 \end{coq_example}