parametres inductifs

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

2 files changed, 22 insertions, 12 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 67a0f850cc..218d7f8228 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -353,7 +353,8 @@ let array_min nmr a = if nmr = 0 then 0 else
 (* The recursive function that checks positivity and builds the list
    of recursive arguments *)
 let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
-  let nparams = rel_context_length hyps in
+  let lparams = rel_context_length hyps in
+  let nmr = rel_context_nhyps hyps in
   (* check the inductive types occur positively in [c] *)
   let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c = 
     let x,largs = decompose_app (whd_betadeltaiota env c) in
@@ -453,31 +454,32 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
      Array.map
       (fun c ->
         let c = body_of_type c in
-        let sign, rawc = mind_extract_params nparams c in
+        let sign, rawc = mind_extract_params lparams c in
         try
-	  check_constructors ienv true nparams rawc
+	  check_constructors ienv true nmr rawc
         with IllFormedInd err -> 
-	  explain_ind_err (ntypes-i) env nparams c err)
+	  explain_ind_err (ntypes-i) env lparams c err)
       indlc
   in
   let irecargs = Array.map snd irecargs_nmr
-  and nmr' = array_min nparams irecargs_nmr
+  and nmr' = array_min nmr irecargs_nmr
   in (nmr', mk_paths (Mrec i) irecargs)
 
 let check_positivity env_ar params inds =
   let ntypes = Array.length inds in
   let lra_ind =
     List.rev (list_tabulate (fun j -> (Mrec j, Rtree.mk_param j)) ntypes) in
-  let nparams = rel_context_length params in
+  let lparams = rel_context_length params in
+  let nmr = rel_context_nhyps params in
   let check_one i (_,_,_,_,_,lc) =
     let ra_env =
-      list_tabulate (fun _ -> (Norec,mk_norec)) nparams @ lra_ind in
-    let ienv = (env_ar, 1+nparams, ntypes, ra_env) in
+      list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
+    let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
     check_positivity_one ienv params i lc 
   in
   let irecargs_nmr = Array.mapi check_one inds in 
   let irecargs = Array.map snd irecargs_nmr
-  and nmr' = array_min nparams irecargs_nmr
+  and nmr' = array_min nmr irecargs_nmr
   in (nmr',Rtree.mk_rec irecargs)
 
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 235c82b1a8..b5d825e843 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -152,11 +152,16 @@ let get_arity mib mip params =
   let arity = mip.mind_nf_arity in
   destArity (full_inductive_instantiate mib params arity)
 
+let rel_list n m = 
+  let rec reln l p = 
+    if p>m then l else reln (mkRel(n+p)::l) (p+1)
+  in 
+  reln [] 1
+
 let build_dependent_inductive ind mib mip params =
-  let arsign,_ = get_arity mib mip params in
   let nrealargs = mip.mind_nrealargs in
   applist 
-    (mkInd ind, (List.map (lift nrealargs) params)@(local_rels arsign))
+    (mkInd ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
 
 
 (* This exception is local *)
@@ -166,6 +171,7 @@ let is_correct_arity env c pj ind mib mip params =
   let kelim = mip.mind_kelim in
   let arsign,s = get_arity mib mip params in
   let nodep_ar = it_mkProd_or_LetIn (mkSort s) arsign in
+  let nrealargs = mip.mind_nrealargs in
   let rec srec env pt t u =
     let pt' = whd_betadeltaiota env pt in
     let t' = whd_betadeltaiota env t in
@@ -180,7 +186,9 @@ let is_correct_arity env c pj ind mib mip params =
           let ksort = match kind_of_term k with
             | Sort s -> family_of_sort s 
 	    | _ -> raise (LocalArity None) in
-	  let dep_ind = build_dependent_inductive ind mib mip params in
+
+	  let dep_ind = build_dependent_inductive ind mib mip params
+	  in 
           let univ =
             try conv env a1 dep_ind
             with NotConvertible -> raise (LocalArity None) in