Fixing bug using explictly declared implicit arguments in inductive arities.

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

2 files changed, 18 insertions, 2 deletions

diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index ce3e692f4a..f446cd2dfa 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -107,3 +107,19 @@ Context {A:Set}.
 Definition h (a:A) := a.
 End C.
 Check h 0.
+
+(* Check implicit arguments in arity of inductive types. The three
+   following examples used to fail before r13671 *)
+
+Inductive I {A} (a:A) : forall {n:nat}, Prop :=
+ | C : I a (n:=0).
+
+Inductive I2 (x:=0) : Prop :=
+ | C2 {p:nat} : p = 0 -> I2.
+Check C2 eq_refl.
+
+Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
+ | C3 : I3 a (n:=0).
+
+Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
+ | C2 {p} : I2 a (n:=p).
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3f4f153187..2e6fd8f498 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -239,7 +239,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
   let env_ar_params = push_rel_context ctx_params env_ar in
 
   (* Compute interpretation metadatas *)
-  let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (List.length userimpls) impls) arities in
+  let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (rel_context_nhyps ctx_params) impls) arities in
   let arities = List.map fst arities in
   let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
@@ -273,7 +273,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
     mind_entry_lc = ctypes
   }) indl arities constructors in
   let impls =
-    let len = List.length ctx_params in
+    let len = rel_context_nhyps ctx_params in
       List.map2 (fun indimpls (_,_,cimpls) ->
 	indimpls, List.map (fun impls ->
 	  userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors