aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/closure.ml4
-rw-r--r--kernel/declarations.ml6
-rw-r--r--kernel/indtypes.ml8
-rw-r--r--kernel/inductive.ml14
-rw-r--r--kernel/modops.ml4
-rw-r--r--kernel/names.ml2
-rw-r--r--kernel/pre_env.ml4
-rw-r--r--kernel/sign.ml4
-rw-r--r--kernel/subtyping.ml2
-rw-r--r--kernel/univ.ml20
10 files changed, 34 insertions, 34 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 94980b5964..210dbb02ba 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -455,7 +455,7 @@ let rec compact_constr (lg, subs as s) c k =
match kind_of_term c with
Rel i ->
if i < k then c,s else
- (try mkRel (k + lg - list_index (i-k+1) subs), (lg,subs)
+ (try mkRel (k + lg - List.index (i-k+1) subs), (lg,subs)
with Not_found -> mkRel (k+lg), (lg+1, (i-k+1)::subs))
| (Sort _|Var _|Meta _|Ind _|Const _|Construct _) -> c,s
| Evar(ev,v) ->
@@ -734,7 +734,7 @@ let rec get_args n tys f e stk =
let eargs = Array.sub l n (na-n) in
(Inl (subs_cons(args,e)), Zapp eargs :: s)
else (* more lambdas *)
- let etys = list_skipn na tys in
+ let etys = List.skipn na tys in
get_args (n-na) etys f (subs_cons(l,e)) s
| _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 5f677d0565..a2ce4f2705 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -110,7 +110,7 @@ let subst_rel_declaration sub (id,copt,t as x) =
let t' = subst_mps sub t in
if copt == copt' & t == t' then x else (id,copt',t')
-let subst_rel_context sub = list_smartmap (subst_rel_declaration sub)
+let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
(* TODO: these substitution functions could avoid duplicating things
when the substitution have preserved all the fields *)
@@ -141,11 +141,11 @@ let hcons_rel_decl ((n,oc,t) as d) =
and t' = hcons_types t
in if n' == n && oc' == oc && t' == t then d else (n',oc',t')
-let hcons_rel_context l = list_smartmap hcons_rel_decl l
+let hcons_rel_context l = List.smartmap hcons_rel_decl l
let hcons_polyarity ar =
{ poly_param_levels =
- list_smartmap (Option.smartmap hcons_univ) ar.poly_param_levels;
+ List.smartmap (Option.smartmap hcons_univ) ar.poly_param_levels;
poly_level = hcons_univ ar.poly_level }
let hcons_const_type = function
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 6c7f4408f7..b93b9f19b1 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -351,7 +351,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
let compute_rec_par (env,n,_,_) hyps nmr largs =
if nmr = 0 then 0 else
(* start from 0, hyps will be in reverse order *)
- let (lpar,_) = list_chop nmr largs in
+ let (lpar,_) = List.chop nmr largs in
let rec find k index =
function
([],_) -> nmr
@@ -375,7 +375,7 @@ let abstract_mind_lc env ntyps npars lc =
lc
else
let make_abs =
- list_tabulate
+ List.tabulate
(function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps
in
Array.map (substl make_abs) lc
@@ -457,7 +457,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
let auxnpar = mib.mind_nparams_rec in
let nonrecpar = mib.mind_nparams - auxnpar in
let (lpar,auxlargs) =
- try list_chop auxnpar largs
+ try List.chop auxnpar largs
with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in
(* If the inductive appears in the args (non params) then the
definition is not positive. *)
@@ -539,7 +539,7 @@ let check_positivity kn env_ar params inds =
let nmr = rel_context_nhyps params in
let check_one i (_,lcnames,lc,(sign,_)) =
let ra_env =
- list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
+ List.tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
let nargs = rel_context_nhyps sign - nmr in
check_positivity_one ienv params (kn,i) nargs lcnames lc
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 58689a9263..d86abb435f 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
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 5eddb6c843..19075058a6 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -562,7 +562,7 @@ and clean_expr l = function
if str_clean == str && sig_clean = sigt.typ_expr then
s else SEBfunctor (mbid,{sigt with typ_expr=sig_clean},str_clean)
| SEBstruct str as s->
- let str_clean = Util.list_smartmap (clean_struct l) str in
+ let str_clean = Util.List.smartmap (clean_struct l) str in
if str_clean == str then s else SEBstruct(str_clean)
| str -> str
@@ -572,7 +572,7 @@ let rec collect_mbid l = function
if str_clean == str then s else
SEBfunctor (mbid,sigt,str_clean)
| SEBstruct str as s->
- let str_clean = Util.list_smartmap (clean_struct l) str in
+ let str_clean = Util.List.smartmap (clean_struct l) str in
if str_clean == str then s else SEBstruct(str_clean)
| _ -> anomaly "Modops:the evaluation of the structure failed "
diff --git a/kernel/names.ml b/kernel/names.ml
index d7b9516ae0..aa5313842d 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -369,7 +369,7 @@ module Hdir = Hashcons.Make(
struct
type t = dir_path
type u = identifier -> identifier
- let hash_sub hident d = list_smartmap hident d
+ let hash_sub hident d = List.smartmap hident d
let rec equal d1 d2 =
(d1==d2) ||
match (d1,d2) with
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 3d2f19aac8..476a92bedc 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -93,8 +93,8 @@ let lookup_rel_val n env =
let env_of_rel n env =
{ env with
- env_rel_context = Util.list_skipn n env.env_rel_context;
- env_rel_val = Util.list_skipn n env.env_rel_val;
+ env_rel_context = Util.List.skipn n env.env_rel_context;
+ env_rel_val = Util.List.skipn n env.env_rel_val;
env_nb_rel = env.env_nb_rel - n
}
diff --git a/kernel/sign.ml b/kernel/sign.ml
index a654bc04dd..269f7a5d96 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -34,7 +34,7 @@ let rec lookup_named id = function
| [] -> raise Not_found
let named_context_length = List.length
-let named_context_equal = list_equal eq_named_declaration
+let named_context_equal = List.equal eq_named_declaration
let vars_of_named_context = List.map (fun (id,_,_) -> id)
@@ -61,7 +61,7 @@ let map_context f l =
if body_o' == body_o && typ' == typ then decl else
(n, body_o', typ')
in
- list_smartmap map_decl l
+ List.smartmap map_decl l
let map_rel_context = map_context
let map_named_context = map_context
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 5fec0c2c7e..c590a51015 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -198,7 +198,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
check (fun mib ->
let nparamdecls = List.length mib.mind_params_ctxt in
let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in
- snd (list_chop nparamdecls names))
+ snd (List.chop nparamdecls names))
(fun x -> RecordProjectionsExpected x);
end;
(* we first check simple things *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1f864926a4..9334a06d13 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -130,12 +130,12 @@ let sup u v =
if UniverseLevel.equal u v then Atom u else Max ([u;v],[])
| u, Max ([],[]) -> u
| Max ([],[]), v -> v
- | Atom u, Max (gel,gtl) -> Max (list_add_set u gel,gtl)
- | Max (gel,gtl), Atom v -> Max (list_add_set v gel,gtl)
+ | Atom u, Max (gel,gtl) -> Max (List.add_set u gel,gtl)
+ | Max (gel,gtl), Atom v -> Max (List.add_set v gel,gtl)
| Max (gel,gtl), Max (gel',gtl') ->
- let gel'' = list_union gel gel' in
- let gtl'' = list_union gtl gtl' in
- Max (list_subtract gel'' gtl'',gtl'')
+ let gel'' = List.union gel gel' in
+ let gtl'' = List.union gtl gtl' in
+ Max (List.subtract gel'' gtl'',gtl'')
(* Comparison on this type is pointer equality *)
type canonical_arc =
@@ -423,7 +423,7 @@ let merge g arcu arcv =
(* redirected to it *)
let redirect (g,w,w') arcv =
let g' = enter_equiv_arc arcv.univ arcu.univ g in
- (g',list_unionq arcv.lt w,arcv.le@w')
+ (g',List.unionq arcv.lt w,arcv.le@w')
in
let (g',w,w') = List.fold_left redirect (g,[],[]) v in
let g_arcu = (g',arcu) in
@@ -759,7 +759,7 @@ let make_max = function
let remove_large_constraint u = function
| Atom u' as x -> if u = u' then Max ([],[]) else x
- | Max (le,lt) -> make_max (list_remove u le,lt)
+ | Max (le,lt) -> make_max (List.remove u le,lt)
let is_direct_constraint u = function
| Atom u' -> u = u'
@@ -900,8 +900,8 @@ module Huniv =
match u, v with
| Atom u, Atom v -> u == v
| Max (gel,gtl), Max (gel',gtl') ->
- (list_for_all2eq (==) gel gel') &&
- (list_for_all2eq (==) gtl gtl')
+ (List.for_all2eq (==) gel gel') &&
+ (List.for_all2eq (==) gtl gtl')
| _ -> false
let hash = Hashtbl.hash
end)
@@ -928,7 +928,7 @@ module Hconstraints =
let hash_sub huc s =
Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
let equal s s' =
- list_for_all2eq (==)
+ List.for_all2eq (==)
(Constraint.elements s)
(Constraint.elements s')
let hash = Hashtbl.hash
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 16:47:24 +0000