Inductive parameters: nicer doc examples and error message

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

2 files changed, 15 insertions, 15 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index a7e3e279ea..833aefa2c3 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -559,7 +559,7 @@ $\Gamma_C$.
 \paragraph{Examples.}
 The inductive declaration for the type of natural numbers will be:
 \[\NInd{}{\nat:\Set}{\nO:\nat,\nS:\nat\ra\nat}\]
-In a context with a variable $A:\Set$, the lists of elements in $A$ is
+In a context with a variable $A:\Set$, the lists of elements in $A$ are
 represented by:
 \[\NInd{A:\Set}{\List:\Set}{\Nil:\List,\cons : A \ra \List \ra
   \List}\]
@@ -577,8 +577,8 @@ represented by:
 
 We have to slightly complicate the representation above in order to handle
 the delicate problem of parameters. 
-Let us explain that on the example of \List. As they were defined
-above, the type \List\ can only be used in an environment where we
+Let us explain that on the example of \List. With the above definition,
+the type \List\ can only be used in an environment where we
 have a variable $A:\Set$. Generally one want to consider lists of
 elements in different types. For constants this is easily done by abstracting
 the value over the parameter. In the case of inductive definitions we
@@ -586,8 +586,8 @@ have to handle the abstraction over several objects.
 
 One possible way to do that would be to define the type \List\
 inductively as being an inductive family of type $\Set\ra\Set$:
-\[\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
-  \ra (\List~A) \ra (\List~A)}\]
+\[\NInd{}{\List:\Set\ra\Set}{\Nil:(\forall A:\Set,\List~A),
+  \cons : (\forall A:\Set, A \ra \List~A \ra \List~A)}\]
 There are drawbacks to this point of view. The
 information which says that for any $A$, $(\List~A)$ is an inductively defined
 \Set\ has been lost.
@@ -619,15 +619,15 @@ type $T$ of $t$: these are exactly the $r$ first arguments of $I$ in
 the head normal form of $T$.
 \paragraph{Examples.}
 The \List{} definition has $1$ parameter:
-\[\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
-  \ra (\List~A) \ra (\List~A)}\]
+\[\NInd{}{\List:\Set\ra\Set}{\Nil:(\forall A:\Set, \List~A),
+  \cons : (\forall A:\Set, A \ra \List~A \ra \List~A)}\]
 This is also the case for this more complex definition where there is
 a recursive argument on a different instance of \List: 
-\[\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
-           \ra (\List~A\ra A) \ra (\List~A)}\]
+\[\NInd{}{\List:\Set\ra\Set}{\Nil:(\forall A:\Set, \List~A),
+  \cons : (\forall A:\Set, A \ra \List~(A \ra A) \ra \List~A)}\]
 But the following definition has $0$ parameters:
-\[\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
-           \ra (\List~A) \ra (\List~A*A)}\]
+\[\NInd{}{\List:\Set\ra\Set}{\Nil:(\forall A:\Set, \List~A),
+  \cons : (\forall A:\Set, A \ra \List~A \ra \List~(A*A))}\]
 
 %\footnote{
 %The interested reader may compare the above definition with the two 
@@ -671,8 +671,8 @@ when $p$ is (less or equal than) the number of parameters in
 
 \paragraph{Examples}
 The declaration for parameterized lists is:
-\[\Ind{}{1}{\List:\Set\ra\Set}{\Nil:\forall A:\Set,\List~A,\cons : \forall
-  A:\Set, A \ra \List~A \ra   \List~A}\]
+\[\Ind{}{1}{\List:\Set\ra\Set}{\Nil:(\forall A:\Set,\List~A),\cons :
+  (\forall A:\Set, A \ra \List~A \ra   \List~A)}\]
 
 The declaration for the length of lists is:
 \[\Ind{}{1}{\Length:\forall A:\Set, (\List~A)\ra \nat\ra\Prop}
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 26c29d4c0f..1bc4e4f33c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -633,8 +633,8 @@ let error_bad_ind_parameters env c n v1 v2  =
   let pc = pr_lconstr_env_at_top env c in
   let pv1 = pr_lconstr_env env v1 in
   let pv2 = pr_lconstr_env env v2 in
-  str "The " ++ nth n ++ str " argument of " ++ pv2 ++ brk(1,1) ++
-  str "must be " ++ pv1 ++ str " in" ++ brk(1,1) ++ pc ++ str "."
+  str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++
+  str " as " ++ nth n ++ str " argument in " ++ brk(1,1) ++ pc ++ str "."
 
 let error_same_names_types id =
   str "The name" ++ spc () ++ pr_id id ++ spc () ++