ajout d'une passe de latex our avoir un index correct

+ quelques petites retouches sur la doc


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

1 files changed, 28 insertions, 31 deletions

diff --git a/doc/Tutorial.tex b/doc/Tutorial.tex
index 0e43247cf6..7b30a82940 100755
--- a/doc/Tutorial.tex
+++ b/doc/Tutorial.tex
@@ -47,7 +47,7 @@ The standard invocation of \Coq\ delivers a message such as:
 \begin{flushleft}
 \begin{verbatim}
 unix:~> coqtop
-Welcome to Coq 8.0 (Dec 2003)
+Welcome to Coq 8.0 (Feb 2004)
 
 Coq < 
 \end{verbatim}
@@ -458,7 +458,7 @@ Actually, the tactic \verb+Split+ is just an abbreviation for \verb+apply conj.+
 What we have just seen is that the \verb:auto: tactic is more powerful than
 just a simple application of local hypotheses; it tries to apply as well 
 lemmas which have been specified as hints. A 
-\verb:Hints Resolve: command registers a
+\verb:Hint Resolve: command registers a
 lemma as a hint to be used from now on by the \verb:auto: tactic, whose power 
 may thus be incrementally augmented.
 
@@ -763,7 +763,7 @@ theorem in the first-order language declared in section
 \verb:R_sym_trans: has not been really significant, since we could have
 instead stated theorem \verb:refl_if: in its general form, and done 
 basically the same proof, obtaining \verb:R_symmetric: and
-\verb:R_transitive: as local hypotheses by initial \verb:Intros: rather
+\verb:R_transitive: as local hypotheses by initial \verb:intros: rather
 than as global hypotheses in the context. But if we had pursued the
 theory by proving more theorems about relation \verb:R:,
 we would have obtained all general statements at the closing of the section,
@@ -787,7 +787,8 @@ Lemma weird : (forall x:D, P x) ->  exists a, P a.
  intro UnivP.
 \end{coq_example}
 
-First of all, notice the pair of parentheses around \verb+(x:D)(P x)+ in
+First of all, notice the pair of parentheses around
+\verb+forall (x:D), P x+ in
 the statement of lemma \verb:weird:.
 If we had omitted them, \Coq's parser would have interpreted the
 statement as a truly trivial fact, since we would 
@@ -884,7 +885,7 @@ Finally, the excluded middle hypothesis is discharged only in
 Note that the name \verb:d: has vanished as well from
 the statements of \verb:weird: and \verb:drinker:, 
 since \Coq's pretty-printer replaces
-systematically a quantification such as \verb+(d:D)E+, where \verb:d:
+systematically a quantification such as \verb+forall d:D, E+, where \verb:d:
 does not occur in \verb:E:, by the functional notation \verb:D->E:. 
 Similarly the name \verb:EM: does not appear in \verb:drinker:. 
 
@@ -962,9 +963,9 @@ Qed.
 \end{coq_example}
 
 When one wants to rewrite an equality in a right to left fashion, we should
-use \verb:Rewrite <- E: rather than \verb:Rewrite E: or the equivalent
-\verb:Rewrite -> E:. 
-Let us now illustrate the tactic \verb:Replace:.
+use \verb:rewrite <- E: rather than \verb:rewrite E: or the equivalent
+\verb:rewrite -> E:. 
+Let us now illustrate the tactic \verb:replace:.
 \begin{coq_example}
 Hypothesis f10 : f 1 = f 0.
 Lemma L2 : f (f 1) = 0.
@@ -974,8 +975,8 @@ What happened here is that the replacement left the first subgoal to be
 proved, but another proof obligation was generated by the \verb:Replace:
 tactic, as the second subgoal. The first subgoal is solved immediately
 by applying lemma \verb:foo:; the second one transitivity and then 
-symmetry of equality, for instance with tactics \verb:Transitivity: and 
-\verb:Symmetry::
+symmetry of equality, for instance with tactics \verb:transitivity: and 
+\verb:symmetry::
 \begin{coq_example}
 apply foo.
 transitivity (f 0); symmetry; trivial.
@@ -1014,9 +1015,8 @@ combinator may be invoked by the tactic \verb:Exists: as above.
 Check ex_intro.
 \end{coq_example}
 
-Similarly, equality over Type is available, with notation 
-\verb:M==N:. The equality tactics process \verb:==: in the same way
-as \verb:=:.
+Equality over Type is available, with notation 
+\verb:M=N:.
 
 \section{Using definitions}
 
@@ -1054,9 +1054,10 @@ relation.
 Lemma subset_transitive : transitive set subset.
 \end{coq_example}
 
-In order to make any progress, one needs to use the definition of 
-\verb:transitive:. The \verb:unfold: tactic, which replaces all occurrences of a
-defined notion by its definition in the current goal, may be used here.
+In order to make any progress, one needs to use the definition of
+\verb:transitive:. The \verb:unfold: tactic, which replaces all
+occurrences of a defined notion by its definition in the current goal,
+may be used here.
 \begin{coq_example}
 unfold transitive.
 \end{coq_example}
@@ -1085,7 +1086,7 @@ intros.
 unfold subset in H.
 \end{coq_example}
 
-Finally, the tactic \verb:Red: does only unfolding of the head occurrence
+Finally, the tactic \verb:red: does only unfolding of the head occurrence
 of the current goal:
 \begin{coq_example}
 red.
@@ -1123,9 +1124,7 @@ mathematical constructions.
 Let us start with the collection of booleans, as they are specified
 in the \Coq's \verb:Prelude: module: 
 \begin{coq_example}
-Inductive bool :  Set :=
-  | true : bool
-  | false : bool.
+Inductive bool :  Set := true | false.
 \end{coq_example}
 
 Such a declaration defines several objects at once. First, a new
@@ -1221,8 +1220,8 @@ Definition addition (n m:nat) := prim_rec m (fun p rec:nat => S rec) n.
 \end{coq_example}
 
 That is, we specify that \verb+(addition n m)+ computes by cases on \verb:n:
-according to its main constructor; when \verb:n=O:, we get \verb:m:;
- when \verb:n=(S p):, we get \verb:(S rec):, where \verb:rec: is the result
+according to its main constructor; when \verb:n = O:, we get \verb:m:;
+ when \verb:n = S p:, we get \verb:(S rec):, where \verb:rec: is the result
 of the recursive computation \verb+(addition p m)+. Let us verify it by
 asking \Coq~to compute for us say $2+3$:
 \begin{coq_example}
@@ -1230,7 +1229,7 @@ Eval compute in (addition (S (S O)) (S (S (S O)))).
 \end{coq_example}
 
 Actually, we do not have to do all explicitly. {\Coq} provides a
-special syntax {\tt Fixpoint/Cases} for generic primitive recursion,
+special syntax {\tt Fixpoint/match} for generic primitive recursion,
 and we could thus have defined directly addition as:
 
 \begin{coq_example}
@@ -1270,12 +1269,12 @@ What happened was that \verb:elim n:, in order to construct a \verb:Prop:
 (the initial goal) from a \verb:nat: (i.e. \verb:n:), appealed to the
 corresponding induction principle \verb:nat_ind: which we saw was indeed
 exactly Peano's induction scheme. Pattern-matching instantiated the 
-corresponding predicate \verb:P: to \verb+[n:nat]n=(plus n O)+, and we get
+corresponding predicate \verb:P: to \verb+fun n:nat => n = n + 0+, and we get
 as subgoals the corresponding instantiations of the base case \verb:(P O): ,
-and of the inductive step \verb+(y:nat)(P y)->(P (S y))+.
+and of the inductive step \verb+forall y:nat, P y -> P (S y)+.
 In each case we get an instance of function \verb:plus: in which its second
 argument starts with a constructor, and is thus amenable to simplification
-by primitive recursion. The \Coq~tactic \verb:Simpl: can be used for
+by primitive recursion. The \Coq~tactic \verb:simpl: can be used for
 this purpose:
 \begin{coq_example}
 simpl.
@@ -1368,8 +1367,8 @@ Lemma no_confusion : forall n:nat, 0 <> S n.
 \end{coq_example}
 
 First of all, we replace negation by its definition, by reducing the
-goal with tactic \verb:Red:; then we get contradiction by successive
-\verb:Intros::
+goal with tactic \verb:red:; then we get contradiction by successive
+\verb:intros::
 \begin{coq_example}
 red; intros n H.
 \end{coq_example}
@@ -1517,13 +1516,11 @@ of the libraries known by Coq, another module is also called
 all its contents, and all the contents of its subdirectories recursively are
 visible and accessible by a short (relative) name as \verb=Arith=.
 Notice also that modules or definitions not explicitly registered in
-a library are put in a default library called \verb=Scratch=.
+a library are put in a default library called \verb=Top=.
 
 The loading of a compiled file is quick, because the corresponding
 development is not type-checked again. 
 
-{\bf Warning}: \Coq~ does not yet provides parametric modules.
-
 \section{Creating your own modules}
 
 You may create your own modules, by writing \Coq~ commands in a file,