From 242e810e149d19d9a6089e6af564acd884b61fc5 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 18 Mar 2008 13:30:04 +0000
Subject: git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10690
 85f007b7-540e-0410-9357-904b9bb8a0f7

---
 kernel/indtypes.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 691992dec9..c299ff5531 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -386,7 +386,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
     push_rel (Anonymous,None,
               hnf_prod_applist env (type_of_inductive env specif) lpar) env in
   let ra_env' = 
-    (Imbr mi,Rtree.mk_param 0) ::
+    (Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
     List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
   (* New index of the inductive types *)
   let newidx = n + auxntyp in
@@ -510,8 +510,8 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc =
 
 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 rc = Array.mapi (fun j t -> (Mrec j,t)) (Rtree.mk_rec_calls ntypes) in
+  let lra_ind = List.rev (Array.to_list rc) in
   let lparams = rel_context_length params in
   let nmr = rel_context_nhyps params in
   let check_one i (_,lcnames,lc,(sign,_)) =
-- 
cgit v1.2.3