aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml8
-rw-r--r--checker/check.mllib1
-rw-r--r--checker/closure.ml4
-rw-r--r--checker/declarations.ml2
-rw-r--r--checker/indtypes.ml8
-rw-r--r--checker/inductive.ml14
-rw-r--r--checker/term.ml2
7 files changed, 20 insertions, 19 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 9e6b635372..5b58dc9baf 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -149,20 +149,20 @@ let canonical_path_name p =
let find_logical_path phys_dir =
let phys_dir = canonical_path_name phys_dir in
- match list_filter2 (fun p d -> p = phys_dir) !load_paths with
+ match List.filter2 (fun p d -> p = phys_dir) !load_paths with
| _,[dir] -> dir
| _,[] -> default_root_prefix
| _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
let remove_load_path dir =
- load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
+ load_paths := List.filter2 (fun p d -> p <> dir) !load_paths
let add_load_path (phys_path,coq_path) =
if !Flags.debug then
ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
str phys_path);
let phys_path = canonical_path_name phys_path in
- match list_filter2 (fun p d -> p = phys_path) !load_paths with
+ match List.filter2 (fun p d -> p = phys_path) !load_paths with
| _,[dir] ->
if coq_path <> dir
(* If this is not the default -I . to coqtop *)
@@ -185,7 +185,7 @@ let add_load_path (phys_path,coq_path) =
| _ -> anomaly ("Two logical paths are associated to "^phys_path)
let load_paths_of_dir_path dir =
- fst (list_filter2 (fun p d -> d = dir) !load_paths)
+ fst (List.filter2 (fun p d -> d = dir) !load_paths)
(************************************************************************)
(*s Locate absolute or partially qualified library names in the path *)
diff --git a/checker/check.mllib b/checker/check.mllib
index 15d7df1d3d..b7e196d4ba 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -7,6 +7,7 @@ Loc
Segmenttree
Unicodetable
Errors
+CList
Util
Option
Hashcons
diff --git a/checker/closure.ml b/checker/closure.ml
index 7f23ed2018..c3351cea13 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -370,7 +370,7 @@ let rec compact_constr (lg, subs as s) c k =
match c with
Rel i ->
if i < k then c,s else
- (try Rel (k + lg - list_index (i-k+1) subs), (lg,subs)
+ (try Rel (k + lg - List.index (i-k+1) subs), (lg,subs)
with Not_found -> Rel (k+lg), (lg+1, (i-k+1)::subs))
| (Sort _|Var _|Meta _|Ind _|Const _|Construct _) -> c,s
| Evar(ev,v) ->
@@ -648,7 +648,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/checker/declarations.ml b/checker/declarations.ml
index ba56c243fb..ad14a3bbe4 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -546,7 +546,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)
type recarg =
| Norec
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index b11b79d1ae..6d936796a6 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -331,7 +331,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
recursive parameters *)
let check_rec_par (env,n,_,_) hyps nrecp largs =
- let (lpar,_) = list_chop nrecp largs in
+ let (lpar,_) = List.chop nrecp largs in
let rec find index =
function
| ([],_) -> ()
@@ -355,7 +355,7 @@ let abstract_mind_lc env ntyps npars lc =
lc
else
let make_abs =
- list_tabulate
+ List.tabulate
(function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps
in
Array.map (substl make_abs) lc
@@ -432,7 +432,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
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. *)
@@ -514,7 +514,7 @@ let check_positivity env_ar mind params nrecp inds =
let lparams = rel_context_length params in
let check_one i mip =
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
check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
in
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 6e87fb3654..f35d68ad1a 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -58,7 +58,7 @@ let inductive_params (mib,_) = mib.mind_nparams
let ind_subst mind mib =
let ntypes = mib.mind_ntypes in
let make_Ik k = Ind (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 =
@@ -255,7 +255,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
(Ind ind,
List.map (lift mip.mind_nrealargs_ctxt) params
@@ -309,7 +309,7 @@ let build_branches_type ind (_,mip as specif) params dep 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 =
if dep then
let cstr = ith_constructor_of_inductive ind (i+1) in
@@ -331,7 +331,7 @@ let build_case_type dep p c realargs =
let type_case_branches env (ind,largs) (p,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 dep = is_correct_arity env c (p,pj) ind specif params in
let lc = build_branches_type ind specif params dep p in
let ty = build_case_type dep p c realargs in
@@ -444,7 +444,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.lazy_from_val Not_subterm)
@@ -527,7 +527,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
@@ -871,7 +871,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/checker/term.ml b/checker/term.ml
index 955a61c147..a7fc0a8b85 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -346,7 +346,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-10 02:30:49 +0000