diff options
| author | barras | 2008-03-18 13:30:04 +0000 |
|---|---|---|
| committer | barras | 2008-03-18 13:30:04 +0000 |
| commit | 242e810e149d19d9a6089e6af564acd884b61fc5 (patch) | |
| tree | ca7b74e6621b9ba79ed5185184080e58172090ea /kernel/indtypes.ml | |
| parent | d4685a5bdaf15c31ddc616777b05280ec7570d08 (diff) | |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10690 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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,_)) = |