diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 58689a926..d86abb435 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -54,7 +54,7 @@ let inductive_params (mib,_) = mib.mind_nparams let ind_subst mind mib = let ntypes = mib.mind_ntypes in let make_Ik k = mkInd (mind,ntypes-k-1) in - list_tabulate make_Ik ntypes + List.tabulate make_Ik ntypes (* Instantiate inductives in constructor type *) let constructor_instantiate mind mib c = @@ -272,7 +272,7 @@ let extended_rel_list n hyps = reln [] 1 hyps let build_dependent_inductive ind (_,mip) params = - let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in + let realargs,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in applist (mkInd ind, List.map (lift mip.mind_nrealargs_ctxt) params @@ -327,7 +327,7 @@ let build_branches_type ind (_,mip as specif) params p = let (args,ccl) = decompose_prod_assum typi in let nargs = rel_context_length args in let (_,allargs) = decompose_app ccl in - let (lparams,vargs) = list_chop (inductive_params specif) allargs in + let (lparams,vargs) = List.chop (inductive_params specif) allargs in let cargs = let cstr = ith_constructor_of_inductive ind (i+1) in let dep_cstr = applist (mkConstruct cstr,lparams@(local_rels args)) in @@ -344,7 +344,7 @@ let build_case_type n p c realargs = let type_case_branches env (ind,largs) pj c = let specif = lookup_mind_specif env ind in let nparams = inductive_params specif in - let (params,realargs) = list_chop nparams largs in + let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in let univ = is_correct_arity env c pj ind specif params in let lc = build_branches_type ind specif params p in @@ -451,7 +451,7 @@ let push_var renv (x,ty,spec) = genv = spec:: renv.genv } let assign_var_spec renv (i,spec) = - { renv with genv = list_assign renv.genv (i-1) spec } + { renv with genv = List.assign renv.genv (i-1) spec } let push_var_renv renv (x,ty) = push_var renv (x,ty,lazy Not_subterm) @@ -521,7 +521,7 @@ let branches_specif renv c_spec ci = vra | Dead_code -> Array.create nca Dead_code | _ -> Array.create nca Not_subterm) in - list_tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca) + List.tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca) car (* [subterm_specif renv t] computes the recursive structure of [t] and @@ -870,7 +870,7 @@ let check_one_cofix env nbfix def deftype = let lra = vlra.(i-1) in let mI = inductive_of_constructor cstr_kn in let (mib,mip) = lookup_mind_specif env mI in - let realargs = list_skipn mib.mind_nparams args in + let realargs = List.skipn mib.mind_nparams args in let rec process_args_of_constr = function | (t::lr), (rar::lrar) -> if rar = mk_norec then |