aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml42
-rw-r--r--pretyping/cbv.ml4
-rw-r--r--pretyping/classops.ml2
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/detyping.ml18
-rw-r--r--pretyping/evarconv.ml8
-rw-r--r--pretyping/evarutil.ml26
-rw-r--r--pretyping/evd.ml8
-rw-r--r--pretyping/glob_ops.ml8
-rw-r--r--pretyping/indrec.ml6
-rw-r--r--pretyping/inductiveops.ml12
-rw-r--r--pretyping/matching.ml4
-rw-r--r--pretyping/patternops.ml14
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--pretyping/recordops.ml4
-rw-r--r--pretyping/redops.ml4
-rw-r--r--pretyping/reductionops.ml22
-rw-r--r--pretyping/tacred.ml28
-rw-r--r--pretyping/termops.ml14
-rw-r--r--pretyping/typeclasses.ml16
-rw-r--r--pretyping/typing.ml2
21 files changed, 124 insertions, 124 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 163675dfb3..196f5a0e7e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -98,7 +98,7 @@ let msg_may_need_inversion () =
(* Utils *)
let make_anonymous_patvars n =
- list_make n (PatVar (Loc.ghost,Anonymous))
+ List.make n (PatVar (Loc.ghost,Anonymous))
(* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
@@ -295,7 +295,7 @@ let try_find_ind env sigma typ realnames =
let names =
match realnames with
| Some names -> names
- | None -> list_make (List.length realargs) Anonymous in
+ | None -> List.make (List.length realargs) Anonymous in
IsInd (typ,ind,names)
let inh_coerce_to_ind evdref env ty tyi =
@@ -515,7 +515,7 @@ let mk_dep_patt_row (pats,_,eqn) =
let dependencies_in_pure_rhs nargs eqns =
if eqns = [] && not (Flags.is_program_mode ()) then
- list_make nargs false (* Only "_" patts *) else
+ List.make nargs false (* Only "_" patts *) else
let deps_rows = List.map mk_dep_patt_row eqns in
let deps_columns = matrix_transpose deps_rows in
List.map (List.exists ((=) true)) deps_columns
@@ -531,7 +531,7 @@ let rec dep_in_tomatch n = function
let dependencies_in_rhs nargs current tms eqns =
match kind_of_term current with
- | Rel n when dep_in_tomatch n tms -> list_make nargs true
+ | Rel n when dep_in_tomatch n tms -> List.make nargs true
| _ -> dependencies_in_pure_rhs nargs eqns
(* Computing the matrix of dependencies *)
@@ -551,7 +551,7 @@ let rec find_dependency_list tmblock = function
| (used,tdeps,d)::rest ->
let deps = find_dependency_list tmblock rest in
if used && List.exists (fun x -> dependent_decl x d) tmblock
- then list_add_set (List.length rest + 1) (list_union deps tdeps)
+ then List.add_set (List.length rest + 1) (List.union deps tdeps)
else deps
let find_dependencies is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist =
@@ -680,7 +680,7 @@ let merge_name get_name obj = function
let merge_names get_name = List.map2 (merge_name get_name)
let get_names env sign eqns =
- let names1 = list_make (List.length sign) Anonymous in
+ let names1 = List.make (List.length sign) Anonymous in
(* If any, we prefer names used in pats, from top to bottom *)
let names2,aliasname =
List.fold_right
@@ -691,7 +691,7 @@ let get_names env sign eqns =
(* Otherwise, we take names from the parameters of the constructor but
avoiding conflicts with user ids *)
let allvars =
- List.fold_left (fun l (_,_,eqn) -> list_union l eqn.rhs.avoid_ids)
+ List.fold_left (fun l (_,_,eqn) -> List.union l eqn.rhs.avoid_ids)
[] eqns in
let names3,_ =
List.fold_left2
@@ -723,7 +723,7 @@ let push_rels_eqn sign eqn =
rhs = {eqn.rhs with rhs_env = push_rel_context sign eqn.rhs.rhs_env} }
let push_rels_eqn_with_names sign eqn =
- let subpats = List.rev (list_firstn (List.length sign) eqn.patterns) in
+ let subpats = List.rev (List.firstn (List.length sign) eqn.patterns) in
let subpatnames = List.map alias_of_pat subpats in
let sign = recover_initial_subpattern_names subpatnames sign in
push_rels_eqn sign eqn
@@ -1134,7 +1134,7 @@ let build_branch current realargs deps (realnames,curname) pb arsign eqns const_
(* We adjust the terms to match in the context they will be once the *)
(* context [x1:T1,..,xn:Tn] will have been pushed on the current env *)
let typs' =
- list_map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 typs in
+ List.map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 typs in
let extenv = push_rel_context typs pb.env in
@@ -1462,7 +1462,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
| Evar ev ->
let ty = get_type_of env sigma t in
let inst =
- list_map_i
+ List.map_i
(fun i _ ->
try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
1 (rel_context env) in
@@ -1477,7 +1477,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
let ty = lift (-k) (aux x (get_type_of env !evdref t)) in
let depvl = free_rels ty in
let inst =
- list_map_i
+ List.map_i
(fun i _ -> if List.mem i vl then u else mkRel i) 1
(rel_context extenv) in
let rel_filter =
@@ -1534,15 +1534,15 @@ let build_inversion_problem loc env sigma tms t =
| App (f,v) when isConstruct f ->
let cstr = destConstruct f in
let n = constructor_nrealargs env cstr in
- let l = list_lastn n (Array.to_list v) in
- let l,acc = list_fold_map' reveal_pattern l acc in
+ let l = List.lastn n (Array.to_list v) in
+ let l,acc = List.fold_map' reveal_pattern l acc in
PatCstr (Loc.ghost,cstr,l,Anonymous), acc
| _ -> make_patvar t acc in
let rec aux n env acc_sign tms acc =
match tms with
| [] -> [], acc_sign, acc
| (t, IsInd (_,IndType(indf,realargs),_)) :: tms ->
- let patl,acc = list_fold_map' reveal_pattern realargs acc in
+ let patl,acc = List.fold_map' reveal_pattern realargs acc in
let pat,acc = make_patvar t acc in
let indf' = lift_inductive_family n indf in
let sign = make_arity_signature env true indf' in
@@ -1570,14 +1570,14 @@ let build_inversion_problem loc env sigma tms t =
let n = List.length sign in
let decls =
- list_map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 sign in
+ List.map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 sign in
let pb_env = push_rel_context sign env in
let decls =
List.map (fun (c,d) -> (c,extract_inductive_data pb_env sigma d,d)) decls in
let decls = List.rev decls in
- let dep_sign = find_dependencies_signature (list_make n true) decls in
+ let dep_sign = find_dependencies_signature (List.make n true) decls in
let sub_tms =
List.map2 (fun deps (tm,(tmtyp,_),(na,b,t)) ->
@@ -1664,7 +1664,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
if nrealargs_ctxt <> List.length realnal then
anomaly "Ill-formed 'in' clause in cases";
List.rev realnal
- | None -> list_make nrealargs_ctxt Anonymous in
+ | None -> List.make nrealargs_ctxt Anonymous in
(na,None,build_dependent_inductive env0 indf')
::(List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign) in
let rec buildrec n = function
@@ -2273,11 +2273,11 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
let dep_sign =
find_dependencies_signature
- (list_make (List.length typs) true)
+ (List.make (List.length typs) true)
typs in
let typs' =
- list_map3
+ List.map3
(fun (tm,tmt) deps na ->
let deps = if not (isRel tm) then [] else deps in
((tm,tmt),deps,na))
@@ -2346,11 +2346,11 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
let dep_sign =
find_dependencies_signature
- (list_make (List.length typs) true)
+ (List.make (List.length typs) true)
typs in
let typs' =
- list_map3
+ List.map3
(fun (tm,tmt) deps na ->
let deps = if not (isRel tm) then [] else deps in
((tm,tmt),deps,na))
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index fd88049b24..099a2ab76f 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -262,7 +262,7 @@ and cbv_stack_term info stack env t =
let eargs = Array.sub args nlams (nargs-nlams) in
cbv_stack_term info (APP(eargs,stk)) env' b
else
- let ctxt' = list_skipn nargs ctxt in
+ let ctxt' = List.skipn nargs ctxt in
LAM(nlams-nargs,ctxt', b, subs_cons(args,env))
(* a Fix applied enough -> IOTA *)
@@ -328,7 +328,7 @@ and cbv_norm_value info = function (* reduction under binders *)
map_constr_with_binders subs_lift (cbv_norm_term info) env t
| LAM (n,ctxt,b,env) ->
let nctxt =
- list_map_i (fun i (x,ty) ->
+ List.map_i (fun i (x,ty) ->
(x,cbv_norm_term info (subs_liftn i env) ty)) 0 ctxt in
compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b)
| FIXP ((lij,(names,lty,bds)),env,args) ->
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index a1b7e5e9dd..14476354b3 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -313,7 +313,7 @@ let add_coercion_in_graph (ic,source,target) =
try_add_new_path1 (s,target) (p@[ic]);
Gmap.iter
(fun (u,v) q ->
- if u<>v & u = target && not (list_equal coe_info_typ_equal p q) then
+ if u<>v & u = target && not (List.equal coe_info_typ_equal p q) then
try_add_new_path1 (s,v) (p@[ic]@q))
old_inheritance_graph
end;
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 0b48654b69..0239a7e44d 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -51,7 +51,7 @@ let apply_pattern_coercion loc pat p =
List.fold_left
(fun pat (co,n) ->
let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in
- Glob_term.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
+ Glob_term.PatCstr (loc, co, List.tabulate f (n+1), Anonymous))
pat p
(* raise Not_found if no coercion found *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 50410ad825..d30c1a11fa 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -217,7 +217,7 @@ let lookup_index_as_renamed env t n =
let update_name na ((_,e),c) =
match na with
- | Name _ when force_wildcard () & noccurn (list_index na e) c ->
+ | Name _ when force_wildcard () & noccurn (List.index na e) c ->
Anonymous
| _ ->
na
@@ -240,14 +240,14 @@ let rec build_tree na isgoal e ci cl =
let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in
let cnl = ci.ci_cstr_ndecls in
List.flatten
- (list_tabulate (fun i -> contract_branch isgoal e (cnl.(i),mkpat i,cl.(i)))
+ (List.tabulate (fun i -> contract_branch isgoal e (cnl.(i),mkpat i,cl.(i)))
(Array.length cl))
and align_tree nal isgoal (e,c as rhs) = match nal with
| [] -> [[],rhs]
| na::nal ->
match kind_of_term c with
- | Case (ci,p,c,cl) when c = mkRel (list_index na (snd e))
+ | Case (ci,p,c,cl) when c = mkRel (List.index na (snd e))
& (* don't contract if p dependent *)
computable p (ci.ci_pp_info.ind_nargs) ->
let clauses = build_tree na isgoal e ci cl in
@@ -579,7 +579,7 @@ let rec subst_cases_pattern subst pat =
| PatVar _ -> pat
| PatCstr (loc,((kn,i),j),cpl,n) ->
let kn' = subst_ind subst kn
- and cpl' = list_smartmap (subst_cases_pattern subst) cpl in
+ and cpl' = List.smartmap (subst_cases_pattern subst) cpl in
if kn' == kn && cpl' == cpl then pat else
PatCstr (loc,((kn',i),j),cpl',n)
@@ -596,7 +596,7 @@ let rec subst_glob_constr subst raw =
| GApp (loc,r,rl) ->
let r' = subst_glob_constr subst r
- and rl' = list_smartmap (subst_glob_constr subst) rl in
+ and rl' = List.smartmap (subst_glob_constr subst) rl in
if r' == r && rl' == rl then raw else
GApp(loc,r',rl')
@@ -617,7 +617,7 @@ let rec subst_glob_constr subst raw =
| GCases (loc,sty,rtno,rl,branches) ->
let rtno' = Option.smartmap (subst_glob_constr subst) rtno
- and rl' = list_smartmap (fun (a,x as y) ->
+ and rl' = List.smartmap (fun (a,x as y) ->
let a' = subst_glob_constr subst a in
let (n,topt) = x in
let topt' = Option.smartmap
@@ -625,10 +625,10 @@ let rec subst_glob_constr subst raw =
let sp' = subst_ind subst sp in
if sp == sp' then t else (loc,(sp',i),y)) topt in
if a == a' && topt == topt' then y else (a',(n,topt'))) rl
- and branches' = list_smartmap
+ and branches' = List.smartmap
(fun (loc,idl,cpl,r as branch) ->
let cpl' =
- list_smartmap (subst_cases_pattern subst) cpl
+ List.smartmap (subst_cases_pattern subst) cpl
and r' = subst_glob_constr subst r in
if cpl' == cpl && r' == r then branch else
(loc,idl,cpl',r'))
@@ -656,7 +656,7 @@ let rec subst_glob_constr subst raw =
let ra1' = array_smartmap (subst_glob_constr subst) ra1
and ra2' = array_smartmap (subst_glob_constr subst) ra2 in
let bl' = array_smartmap
- (list_smartmap (fun (na,k,obd,ty as dcl) ->
+ (List.smartmap (fun (na,k,obd,ty as dcl) ->
let ty' = subst_glob_constr subst ty in
let obd' = Option.smartmap (subst_glob_constr subst) obd in
if ty'==ty & obd'==obd then dcl else (na,k,obd',ty')))
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0740068721..9284e2c237 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -117,7 +117,7 @@ let check_conv_record (t1,sk1) (t2,sk2) =
| _ -> raise Not_found in
let us2,extra_args2 =
let l',s' = strip_app sk2_effective in
- let bef,aft = list_chop (List.length us) l' in
+ let bef,aft = List.chop (List.length us) l' in
(bef, append_stack_app_list aft s') in
c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1,
(n,zip(t2,sk2))
@@ -537,7 +537,7 @@ let evar_eqappr_x ts env evd pbty appr1 appr2 =
(* We assume here |l1| <= |l2| *)
let first_order_unification ts env evd (ev1,l1) (term2,l2) =
- let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
+ let (deb2,rest2) = List.chop (List.length l2-List.length l1) l2 in
ise_and evd
(* First compare extra args for better failure message *)
[(fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) rest2 l1);
@@ -639,7 +639,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
| Some _ -> error "Selection of specific occurrences not supported"
| None ->
let evty = set_holes evdref cty subst in
- let instance = snd (list_filter2 (fun b c -> b) (filter,instance)) in
+ let instance = snd (List.filter2 (fun b c -> b) (filter,instance)) in
let evd,ev = new_evar_instance sign !evdref evty ~filter instance in
evdref := evd;
evsref := (fst (destEvar ev),evty)::!evsref;
@@ -761,7 +761,7 @@ let max_undefined_with_candidates evd =
| Some l -> (evk,ev_info,l)::evars) evd [] in
match l with
| [] -> None
- | a::l -> Some (list_last (a::l))
+ | a::l -> Some (List.last (a::l))
let rec solve_unconstrained_evars_with_canditates evd =
(* max_undefined is supposed to return the most recent, hence
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 3256afd28b..0243a57801 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -172,7 +172,7 @@ let collect_evars emap c =
else (* No recursion on the evar instantiation *) acc
| _ ->
fold_constr collrec acc c in
- list_uniquize (collrec [] c)
+ List.uniquize (collrec [] c)
let push_dependent_evars sigma emap =
Evd.fold_undefined (fun ev {evar_concl = ccl} (sigma',emap') ->
@@ -242,7 +242,7 @@ let apply_subfilter filter subfilter =
filter ([], List.rev subfilter))
let extract_subfilter initial_filter refined_filter =
- snd (list_filter2 (fun b1 b2 -> b1) (initial_filter,refined_filter))
+ snd (List.filter2 (fun b1 b2 -> b1) (initial_filter,refined_filter))
(**********************)
(* Creating new evars *)
@@ -320,7 +320,7 @@ let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ =
let new_evar_instance sign evd typ ?src ?filter ?candidates instance =
assert (not !Flags.debug ||
- list_distinct (ids_of_named_context (named_context_of_val sign)));
+ List.distinct (ids_of_named_context (named_context_of_val sign)));
let evd,newevk = new_pure_evar evd sign ?src ?filter ?candidates typ in
(evd,mkEvar (newevk,Array.of_list instance))
@@ -333,7 +333,7 @@ let new_evar evd env ?src ?filter ?candidates typ =
let instance =
match filter with
| None -> instance
- | Some filter -> list_filter_with filter instance in
+ | Some filter -> List.filter_with filter instance in
new_evar_instance sign evd typ' ?src ?filter ?candidates instance
let new_type_evar ?src ?filter evd env =
@@ -369,7 +369,7 @@ let restrict_evar_key evd evk filter candidates =
let sign = evar_hyps evi in
let src = evi.evar_source in
let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in
- let ctxt = snd (list_filter2 (fun b c -> b) (filter,evar_context evi)) in
+ let ctxt = snd (List.filter2 (fun b c -> b) (filter,evar_context evi)) in
let id_inst = Array.of_list (List.map (fun (id,_,_) -> mkVar id) ctxt) in
Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk
@@ -501,7 +501,7 @@ let extend_alias (_,b,_) (var_aliases,rel_aliases) =
let expand_alias_once aliases x =
match get_alias_chain_of aliases x with
| [] -> None
- | l -> Some (list_last l)
+ | l -> Some (List.last l)
let expansions_of_var aliases x =
match get_alias_chain_of aliases x with
@@ -744,7 +744,7 @@ let is_unification_pattern_evar env evd (evk,args) l t =
let args = remove_instance_local_defs evd evk (Array.to_list args) in
let n = List.length args in
match find_unification_pattern_args env (args @ l) t with
- | Some l -> Some (list_skipn n l)
+ | Some l -> Some (List.skipn n l)
| _ -> None
else
None
@@ -854,7 +854,7 @@ let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter in
let t_in_env = whd_evar evd t_in_env in
let evd = define_fun env evd (destEvar evar_in_env) t_in_env in
let ids = List.map pi1 (named_context_of_val sign) in
- let inst_in_sign = List.map mkVar (list_filter_with filter ids) in
+ let inst_in_sign = List.map mkVar (List.filter_with filter ids) in
let evar_in_sign = mkEvar (fst (destEvar evar_in_env), Array.of_list inst_in_sign) in
(evd,whd_evar evd evar_in_sign)
@@ -881,7 +881,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
let sign1 = evar_hyps evi1 in
let filter1 = evar_filter evi1 in
let ids1 = List.map pi1 (named_context_of_val sign1) in
- let inst_in_sign = List.map mkVar (list_filter_with filter1 ids1) in
+ let inst_in_sign = List.map mkVar (List.filter_with filter1 ids1) in
let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
let id = next_name_away na avoid in
@@ -1179,9 +1179,9 @@ let filter_candidates evd evk filter candidates =
match candidates,filter with
| None,_ | _, None -> candidates
| Some l, Some filter ->
- let ids = List.map pi1 (list_filter_with filter (evar_context evi)) in
+ let ids = List.map pi1 (List.filter_with filter (evar_context evi)) in
Some (List.filter (fun a ->
- list_subset (Idset.elements (collect_vars a)) ids) l)
+ List.subset (Idset.elements (collect_vars a)) ids) l)
let closure_of_filter evd evk filter =
let evi = Evd.find_undefined evd evk in
@@ -1407,7 +1407,7 @@ let solve_evar_evar ?(force=false) f g env evd (evk1,args1 as ev1) (evk2,args2 a
if are_canonical_instances args1 args2 env then
(* If instances are canonical, we solve the problem in linear time *)
let sign = evar_filtered_context (Evd.find evd evk2) in
- let id_inst = list_map_to_array (fun (id,_,_) -> mkVar id) sign in
+ let id_inst = List.map_to_array (fun (id,_,_) -> mkVar id) sign in
Evd.define evk2 (mkEvar(evk1,id_inst)) evd
else
let evd,ev1,ev2 =
@@ -1476,7 +1476,7 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
| None -> raise NoCandidates
| Some l ->
let l' =
- list_map_filter
+ List.map_filter
(filter_compatible_candidates conv_algo env evd evi args rhs) l in
match l' with
| [] -> error_cannot_unify env evd (mkEvar ev, rhs)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index a73a74f457..7d95e743d0 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -56,7 +56,7 @@ let evar_body evi = evi.evar_body
let evar_filter evi = evi.evar_filter
let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps
let evar_filtered_context evi =
- snd (list_filter2 (fun b c -> b) (evar_filter evi,evar_context evi))
+ snd (List.filter2 (fun b c -> b) (evar_filter evi,evar_context evi))
let evar_env evi =
List.fold_right push_named (evar_filtered_context evi)
(reset_context (Global.env()))
@@ -676,7 +676,7 @@ let rec list_assoc_in_triple x = function
let subst_defined_metas bl c =
let rec substrec c = match kind_of_term c with
- | Meta i -> substrec (list_assoc_snd_in_triple i bl)
+ | Meta i -> substrec (List.assoc_snd_in_triple i bl)
| _ -> map_constr substrec c
in try Some (substrec c) with Not_found -> None
@@ -797,9 +797,9 @@ let evar_dependency_closure n sigma =
if n=0 then l
else
let l' =
- list_map_append (fun (evk,_) ->
+ List.map_append (fun (evk,_) ->
try ExistentialMap.find evk graph with Not_found -> []) l in
- aux (n-1) (list_uniquize (Sort.list order (l@l'))) in
+ aux (n-1) (List.uniquize (Sort.list order (l@l'))) in
aux n (undefined_list sigma)
let pr_evar_map_t depth sigma =
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index a090094aaa..d20afaf403 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -36,7 +36,7 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
let map_glob_constr_left_to_right f = function
| GApp (loc,g,args) ->
let comp1 = f g in
- let comp2 = Util.list_map_left f args in
+ let comp2 = Util.List.map_left f args in
GApp (loc,comp1,comp2)
| GLambda (loc,na,bk,ty,c) ->
let comp1 = f ty in
@@ -52,8 +52,8 @@ let map_glob_constr_left_to_right f = function
GLetIn (loc,na,comp1,comp2)
| GCases (loc,sty,rtntypopt,tml,pl) ->
let comp1 = Option.map f rtntypopt in
- let comp2 = Util.list_map_left (fun (tm,x) -> (f tm,x)) tml in
- let comp3 = Util.list_map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in
+ let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in
+ let comp3 = Util.List.map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in
GCases (loc,sty,comp1,comp2,comp3)
| GLetTuple (loc,nal,(na,po),b,c) ->
let comp1 = Option.map f po in
@@ -66,7 +66,7 @@ let map_glob_constr_left_to_right f = function
let comp3 = f b2 in
GIf (loc,f c,(na,comp1),comp2,comp3)
| GRec (loc,fk,idl,bl,tyl,bv) ->
- let comp1 = Array.map (Util.list_map_left (map_glob_decl_left_to_right f)) bl in
+ let comp1 = Array.map (Util.List.map_left (map_glob_decl_left_to_right f)) bl in
let comp2 = Array.map f tyl in
let comp3 = Array.map f bv in
GRec (loc,fk,idl,comp1,comp2,comp3)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 025f7f6687..f11fb46134 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -134,7 +134,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
let d = (n,Some b,t) in
mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c)
| Ind (_,_) ->
- let realargs = list_skipn nparams largs in
+ let realargs = List.skipn nparams largs in
let base = applist (lift i pk,realargs) in
if depK then
Reduction.beta_appvect
@@ -209,7 +209,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
let d = (n,Some b,t) in
mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
| Ind _ ->
- let realargs = list_skipn nparrec largs
+ let realargs = List.skipn nparrec largs
and arg = appvect (mkRel (i+1), Termops.extended_rel_vect 0 hyps) in
applist(lift i fk,realargs@[arg])
| _ -> assert false
@@ -431,7 +431,7 @@ let mis_make_indrec env sigma listdepkind mib =
mis_make_case_com dep env sigma indi (mibi,mipi) kind
in
(* Body of mis_make_indrec *)
- list_tabulate make_one_rec nrec
+ List.tabulate make_one_rec nrec
(**********************************************************************)
(* This builds elimination predicate for Case tactic *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 19126f01bc..a026f53d4e 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -91,7 +91,7 @@ let mis_nf_constructor_type (ind,mib,mip) j =
and nconstr = Array.length mip.mind_consnames in
let make_Ik k = mkInd ((fst ind),ntypes-k-1) in
if j > nconstr then error "Not enough constructors in the type.";
- substl (list_tabulate make_Ik ntypes) specif.(j-1)
+ substl (List.tabulate make_Ik ntypes) specif.(j-1)
(* Arity of constructors excluding parameters and local defs *)
@@ -219,7 +219,7 @@ let get_constructor (ind,mib,mip,params) j =
let typi = instantiate_params typi params mib.mind_params_ctxt in
let (args,ccl) = decompose_prod_assum typi in
let (_,allargs) = decompose_app ccl in
- let vargs = list_skipn (List.length params) allargs in
+ let vargs = List.skipn (List.length params) allargs in
{ cs_cstr = ith_constructor_of_inductive ind j;
cs_params = params;
cs_nargs = rel_context_length args;
@@ -258,11 +258,11 @@ let get_arity env (ind,params) =
let parsign = mib.mind_params_ctxt in
let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in
if List.length params = rel_context_nhyps parsign - nnonrecparams then
- snd (list_chop nnonrecparams mib.mind_params_ctxt)
+ snd (List.chop nnonrecparams mib.mind_params_ctxt)
else
parsign in
let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
- let arsign,_ = list_chop arproperlength mip.mind_arity_ctxt in
+ let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in
let subst = instantiate_context parsign params in
(substl_rel_context subst arsign, Inductive.inductive_sort_family mip)
@@ -324,7 +324,7 @@ let find_rectype env sigma c =
match kind_of_term t with
| Ind ind ->
let (mib,mip) = Inductive.lookup_mind_specif env ind in
- let (par,rargs) = list_chop mib.mind_nparams l in
+ let (par,rargs) = List.chop mib.mind_nparams l in
IndType((ind, par),rargs)
| _ -> raise Not_found
@@ -406,7 +406,7 @@ let type_case_branches_with_names env indspec p c =
let (ind,args) = indspec in
let (mib,mip as specif) = Inductive.lookup_mind_specif env ind in
let nparams = mib.mind_nparams in
- let (params,realargs) = list_chop nparams args in
+ let (params,realargs) = List.chop nparams args in
let lbrty = Inductive.build_branches_type ind specif params p in
(* Build case type *)
let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index bc9c832ae7..37cbcc0629 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -110,7 +110,7 @@ let dummy_constr = mkProp
let rec make_renaming ids = function
| (Name id,Name _,_)::stk ->
let renaming = make_renaming ids stk in
- (try mkRel (list_index id ids) :: renaming
+ (try mkRel (List.index id ids) :: renaming
with Not_found -> dummy_constr :: renaming)
| (_,_,_)::stk ->
dummy_constr :: make_renaming ids stk
@@ -152,7 +152,7 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
| _ -> error "Only bound indices allowed in second order pattern matching.")
args in
let frels = Intset.elements (free_rels cT) in
- if list_subset frels relargs then
+ if List.subset frels relargs then
constrain (n,([],build_lambda relargs stk cT)) subst
else
raise PatternMatchingFailure
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index c3b03e209d..e4ae1e4b85 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -146,13 +146,13 @@ let instantiate_pattern sigma lvar c =
let ctx,c = List.assoc id lvar in
try
let inst =
- List.map (fun id -> mkRel (list_index (Name id) vars)) ctx in
+ List.map (fun id -> mkRel (List.index (Name id) vars)) ctx in
let c = substl inst c in
snd (pattern_of_constr sigma c)
- with Not_found (* list_index failed *) ->
+ with Not_found (* List.index failed *) ->
let vars =
- list_map_filter (function Name id -> Some id | _ -> None) vars in
- error_instantiate_pattern id (list_subtract ctx vars)
+ List.map_filter (function Name id -> Some id | _ -> None) vars in
+ error_instantiate_pattern id (List.subtract ctx vars)
with Not_found (* List.assoc failed *) ->
x)
| (PFix _ | PCoFix _) -> error ("Non instantiable pattern.")
@@ -183,7 +183,7 @@ let rec subst_pattern subst pat =
if f' == f && args' == args then pat else
PApp (f',args')
| PSoApp (i,args) ->
- let args' = list_smartmap (subst_pattern subst) args in
+ let args' = List.smartmap (subst_pattern subst) args in
if args' == args then pat else
PSoApp (i,args')
| PLambda (name,c1,c2) ->
@@ -219,7 +219,7 @@ let rec subst_pattern subst pat =
let c' = subst_pattern subst c in
if c' == c then br else (i,n,c')
in
- let branches' = list_smartmap subst_branch branches in
+ let branches' = List.smartmap subst_branch branches in
if cip' == cip && typ' == typ && c' == c && branches' == branches
then pat
else PCase(cip', typ', c', branches')
@@ -241,7 +241,7 @@ let err loc pp = user_err_loc (loc,"pattern_of_glob_constr", pp)
let rec pat_of_raw metas vars = function
| GVar (_,id) ->
- (try PRel (list_index (Name id) vars)
+ (try PRel (List.index (Name id) vars)
with Not_found -> PVar id)
| GPatVar (_,(false,n)) ->
metas := n::!metas; PMeta (Some n)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5113236954..0eff92b617 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -79,7 +79,7 @@ let search_guard loc env possible_indexes fixdefs =
let fix = ((indexes, 0),fixdefs) in
try check_fix env fix; raise (Found indexes)
with TypeError _ -> ())
- (list_combinations possible_indexes);
+ (List.combinations possible_indexes);
let errmsg = "Cannot guess decreasing argument of fix." in
if loc = Loc.ghost then error errmsg else
user_err_loc (loc,"search_guard", Pp.str errmsg)
@@ -363,7 +363,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
Array.to_list (Array.mapi
(fun i (n,_) -> match n with
| Some n -> [n]
- | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
+ | None -> List.map_i (fun i _ -> i) 0 ctxtv.(i))
vn)
in
let fixdecls = (names,ftys,fdefs) in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 7c128d245d..96b57ae183 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -65,7 +65,7 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
let projs' =
(* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
(* the first component of subst_con. *)
- list_smartmap
+ List.smartmap
(Option.smartmap (fun kn -> fst (subst_con subst kn)))
projs
in
@@ -227,7 +227,7 @@ let compute_canonical_projections (con,ind) =
let args = snd (decompose_app t) in
let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
lookup_structure ind in
- let params, projs = list_chop p args in
+ let params, projs = List.chop p args in
let lpj = keep_true_projections lpj kl in
let lps = List.combine lpj projs in
let comp =
diff --git a/pretyping/redops.ml b/pretyping/redops.ml
index e10a64dc53..46f6684765 100644
--- a/pretyping/redops.ml
+++ b/pretyping/redops.ml
@@ -18,13 +18,13 @@ let make_red_flag l =
if red.rDelta then
Errors.error
"Cannot set both constants to unfold and constants not to unfold";
- add_flag { red with rConst = Util.list_union red.rConst l } lf
+ add_flag { red with rConst = Util.List.union red.rConst l } lf
| FDeltaBut l :: lf ->
if red.rConst <> [] & not red.rDelta then
Errors.error
"Cannot set both constants to unfold and constants not to unfold";
add_flag
- { red with rConst = Util.list_union red.rConst l; rDelta = true }
+ { red with rConst = Util.List.union red.rConst l; rDelta = true }
lf
in
add_flag
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0b5ad7b0bf..fd9a312fc4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -58,7 +58,7 @@ let rec strip_app = function
let strip_n_app n s =
let apps,s' = strip_app s in
try
- let bef,aft = list_chop n apps in
+ let bef,aft = List.chop n apps in
match aft with
|h::[] -> Some (bef,h,s')
|h::t -> Some (bef,h,append_stack_app_list t s')
@@ -66,7 +66,7 @@ let strip_n_app n s =
with
|Failure _ -> None
let nfirsts_app_of_stack n s =
- let (args, _) = strip_app s in list_firstn n args
+ let (args, _) = strip_app s in List.firstn n args
let list_of_app_stack s =
let (out,s') = strip_app s in
Option.init (s' = []) out
@@ -88,7 +88,7 @@ let rec stack_assign s p c = match s with
if p >= q then
Zapp args :: stack_assign s (p-q) c
else
- (match list_chop p args with
+ (match List.chop p args with
(bef, _::aft) -> Zapp (bef@c::aft) :: s
| _ -> assert false)
| _ -> s
@@ -98,7 +98,7 @@ let rec stack_tail p s =
| Zapp args :: s ->
let q = List.length args in
if p >= q then stack_tail (p-q) s
- else Zapp (list_skipn p args) :: s
+ else Zapp (List.skipn p args) :: s
| _ -> failwith "stack_tail"
let rec stack_nth s p = match s with
| Zapp args :: s ->
@@ -241,13 +241,13 @@ let reducible_mind_case c = match kind_of_term c with
let contract_cofix (bodynum,(types,names,bodies as typedbodies)) =
let nbodies = Array.length bodies in
let make_Fi j = mkCoFix (nbodies-j-1,typedbodies) in
- substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
+ substl (List.tabulate make_Fi nbodies) bodies.(bodynum)
let reduce_mind_case mia =
match kind_of_term mia.mconstr with
| Construct (ind_sp,i) ->
(* let ncargs = (fst mia.mci).(i-1) in*)
- let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
+ let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
applist (mia.mlf.(i-1),real_cargs)
| CoFix cofix ->
let cofix_def = contract_cofix cofix in
@@ -260,7 +260,7 @@ let reduce_mind_case mia =
let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) =
let nbodies = Array.length recindices in
let make_Fi j = mkFix ((recindices,nbodies-j-1),typedbodies) in
- substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
+ substl (List.tabulate make_Fi nbodies) bodies.(bodynum)
let fix_recarg ((recindices,bodynum),_) stack =
assert (0 <= bodynum & bodynum < Array.length recindices);
@@ -338,7 +338,7 @@ let rec whd_state_gen flags ts env sigma =
if red_iota flags then
match strip_app stack with
|args, (Zcase(ci, _, lf)::s') ->
- whrec (lf.(c-1), append_stack_app_list (list_skipn ci.ci_npar args) s')
+ whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
|args, (Zfix (f,s')::s'') ->
let x' = applist(x,args) in
whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
@@ -404,7 +404,7 @@ let local_whd_state_gen flags sigma =
if red_iota flags then
match strip_app stack with
|args, (Zcase(ci, _, lf)::s') ->
- whrec (lf.(c-1), append_stack_app_list (list_skipn ci.ci_npar args) s')
+ whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
|args, (Zfix (f,s')::s'') ->
let x' = applist(x,args) in
whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
@@ -590,7 +590,7 @@ let whd_betaiota_preserving_vm_cast env sigma t =
| Construct (ind,c) -> begin
match strip_app stack with
|args, (Zcase(ci, _, lf)::s') ->
- whrec (lf.(c-1), append_stack_app_list (list_skipn ci.ci_npar args) s')
+ whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
|args, (Zfix (f,s')::s'') ->
let x' = applist(x,args) in
whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
@@ -888,7 +888,7 @@ let whd_programs_stack env sigma =
| Construct (ind,c) -> begin
match strip_app stack with
|args, (Zcase(ci, _, lf)::s') ->
- whrec (lf.(c-1), append_stack_app_list (list_skipn ci.ci_npar args) s')
+ whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
|args, (Zfix (f,s')::s'') ->
let x' = applist(x,args) in
whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9791598fd8..b897c01afb 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -186,12 +186,12 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
raise Elimconst) args
in
let reversible_rels = List.map fst li in
- if not (list_distinct reversible_rels) then
+ if not (List.distinct reversible_rels) then
raise Elimconst;
- list_iter_i (fun i t_i ->
+ List.iter_i (fun i t_i ->
if not (List.mem_assoc (i+1) li) then
let fvs = List.map ((+) (i+1)) (Intset.elements (free_rels t_i)) in
- if list_intersect fvs reversible_rels <> [] then raise Elimconst)
+ if List.intersect fvs reversible_rels <> [] then raise Elimconst)
labs;
let k = lv.(i) in
if k < nargs then
@@ -322,13 +322,13 @@ let reference_eval sigma env = function
let x = Name (id_of_string "x")
let make_elim_fun (names,(nbfix,lv,n)) largs =
- let lu = list_firstn n largs in
+ let lu = List.firstn n largs in
let p = List.length lv in
let lyi = List.map fst lv in
let la =
- list_map_i (fun q aq ->
+ List.map_i (fun q aq ->
(* k from the comment is q+1 *)
- try mkRel (p+1-(list_index (n-q) lyi))
+ try mkRel (p+1-(List.index (n-q) lyi))
with Not_found -> aq)
0 (List.map (lift p) lu)
in
@@ -338,8 +338,8 @@ let make_elim_fun (names,(nbfix,lv,n)) largs =
| Some (minargs,ref) ->
let body = applistc (mkEvalRef ref) la in
let g =
- list_fold_left_i (fun q (* j = n+1-q *) c (ij,tij) ->
- let subst = List.map (lift (-q)) (list_firstn (n-ij) la) in
+ List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) ->
+ let subst = List.map (lift (-q)) (List.firstn (n-ij) la) in
let tij' = substl (List.rev subst) tij in
mkLambda (x,tij',c)) 1 body (List.rev lv)
in Some (minargs,g)
@@ -433,7 +433,7 @@ let reduce_fix whdfun sigma fix stack =
| None -> NotReducible
| Some (recargnum,recarg) ->
let (recarg'hd,_ as recarg') = whdfun sigma recarg in
- let stack' = list_assign stack recargnum (applist recarg') in
+ let stack' = List.assign stack recargnum (applist recarg') in
(match kind_of_term recarg'hd with
| Construct _ -> Reduced (contract_fix fix, stack')
| _ -> NotReducible)
@@ -442,7 +442,7 @@ let contract_fix_use_function env sigma f
((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
let nbodies = Array.length recindices in
let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
- let lbodies = list_tabulate make_Fi nbodies in
+ let lbodies = List.tabulate make_Fi nbodies in
substl_checking_arity env (List.rev lbodies) (nf_beta sigma bodies.(bodynum))
let reduce_fix_use_function env sigma f whfun fix stack =
@@ -455,7 +455,7 @@ let reduce_fix_use_function env sigma f whfun fix stack =
(recarg, [])
else
whfun recarg in
- let stack' = list_assign stack recargnum (applist recarg') in
+ let stack' = List.assign stack recargnum (applist recarg') in
(match kind_of_term recarg'hd with
| Construct _ ->
Reduced (contract_fix_use_function env sigma f fix,stack')
@@ -465,14 +465,14 @@ let contract_cofix_use_function env sigma f
(bodynum,(_names,_,bodies as typedbodies)) =
let nbodies = Array.length bodies in
let make_Fi j = (mkCoFix(j,typedbodies), f j) in
- let subbodies = list_tabulate make_Fi nbodies in
+ let subbodies = List.tabulate make_Fi nbodies in
substl_checking_arity env (List.rev subbodies)
(nf_beta sigma bodies.(bodynum))
let reduce_mind_case_use_function func env sigma mia =
match kind_of_term mia.mconstr with
| Construct(ind_sp,i) ->
- let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
+ let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
applist (mia.mlf.(i-1), real_cargs)
| CoFix (bodynum,(names,_,_) as cofix) ->
let build_cofix_name =
@@ -661,7 +661,7 @@ let rec red_elim_const env sigma ref largs =
let arg = List.nth stack i in
let rarg = whd_construct_stack env sigma arg in
match kind_of_term (fst rarg) with
- | Construct _ -> list_assign stack i (applist rarg)
+ | Construct _ -> List.assign stack i (applist rarg)
| _ -> raise Redelimination)
largs l, n >= 0 && l = [] && nargs >= n,
n >= 0 && l <> [] && nargs >= n in
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index e4f481e58d..765f1e4fa7 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -286,10 +286,10 @@ let adjust_app_list_size f1 l1 f2 l2 =
let len1 = List.length l1 and len2 = List.length l2 in
if len1 = len2 then (f1,l1,f2,l2)
else if len1 < len2 then
- let extras,restl2 = list_chop (len2-len1) l2 in
+ let extras,restl2 = List.chop (len2-len1) l2 in
(f1, l1, applist (f2,extras), restl2)
else
- let extras,restl1 = list_chop (len1-len2) l1 in
+ let extras,restl1 = List.chop (len1-len2) l1 in
(applist (f1,extras), restl1, f2, l2)
let adjust_app_array_size f1 l1 f2 l2 =
@@ -550,7 +550,7 @@ let free_rels m =
let collect_metas c =
let rec collrec acc c =
match kind_of_term c with
- | Meta mv -> list_add_set mv acc
+ | Meta mv -> List.add_set mv acc
| _ -> fold_constr collrec acc c
in
List.rev (collrec [] c)
@@ -691,7 +691,7 @@ let replace_term = replace_term_gen eq_constr
except the ones in l *)
let error_invalid_occurrence l =
- let l = list_uniquize (List.sort Pervasives.compare l) in
+ let l = List.uniquize (List.sort Pervasives.compare l) in
errorlabstrm ""
(str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++
prlist_with_sep spc int l ++ str ".")
@@ -951,7 +951,7 @@ let align_prod_letin c a : rel_context * constr =
let (lc,_,_) = decompose_prod_letin c in
let (la,l,a) = decompose_prod_letin a in
if not (la >= lc) then invalid_arg "align_prod_letin";
- let (l1,l2) = Util.list_chop lc l in
+ let (l1,l2) = Util.List.chop lc l in
l2,it_mkProd_or_LetIn a l1
(* On reduit une serie d'eta-redex de tete ou rien du tout *)
@@ -1045,7 +1045,7 @@ let adjust_subst_to_rel_context sign l =
| _ -> anomaly "Instance and signature do not match"
in aux [] (List.rev sign) l
-let fold_named_context_both_sides f l ~init = list_fold_right_and_left f l init
+let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
let rec mem_named_context id = function
| (id',_,_) :: _ when id=id' -> true
@@ -1098,7 +1098,7 @@ let context_chop k ctx =
(* Do not skip let-in's *)
let env_rel_context_chop k env =
let rels = rel_context env in
- let ctx1,ctx2 = list_chop k rels in
+ let ctx1,ctx2 = List.chop k rels in
push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
ctx1
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 8fd0f768ea..426197af29 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -154,13 +154,13 @@ let subst_class (subst,cl) =
let do_subst_con c = fst (Mod_subst.subst_con subst c)
and do_subst c = Mod_subst.subst_mps subst c
and do_subst_gr gr = fst (subst_global subst gr) in
- let do_subst_ctx ctx = list_smartmap
+ let do_subst_ctx ctx = List.smartmap
(fun (na, b, t) -> (na, Option.smartmap do_subst b, do_subst t))
ctx in
let do_subst_context (grs,ctx) =
- list_smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
+ List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
do_subst_ctx ctx in
- let do_subst_projs projs = list_smartmap (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in
+ let do_subst_projs projs = List.smartmap (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in
{ cl_impl = do_subst_gr cl.cl_impl;
cl_context = do_subst_context cl.cl_context;
cl_props = do_subst_ctx cl.cl_props;
@@ -195,7 +195,7 @@ let discharge_class (_,cl) =
| Some (_, (tc, _)) -> Some (tc.cl_impl, true))
ctx'
in
- list_smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
+ List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
@ newgrs
in grs', discharge_rel_context subst 1 ctx @ ctx' in
let cl_impl' = Lib.discharge_global cl.cl_impl in
@@ -207,7 +207,7 @@ let discharge_class (_,cl) =
{ cl_impl = cl_impl';
cl_context = context;
cl_props = props;
- cl_projs = list_smartmap (fun (x, y, z) -> x, y, Option.smartmap Lib.discharge_con z) cl.cl_projs }
+ cl_projs = List.smartmap (fun (x, y, z) -> x, y, Option.smartmap Lib.discharge_con z) cl.cl_projs }
let rebuild_class cl =
try
@@ -246,7 +246,7 @@ let build_subclasses ~check env sigma glob pri =
| Some (rels, (tc, args)) ->
let instapp = Reductionops.whd_beta sigma (appvectc c (Termops.extended_rel_vect 0 rels)) in
let projargs = Array.of_list (args @ [instapp]) in
- let projs = list_map_filter
+ let projs = List.map_filter
(fun (n, b, proj) ->
match b with
| None -> None
@@ -408,12 +408,12 @@ let add_inductive_class ind =
let instance_constructor cl args =
let lenpars = List.length (List.filter (fun (na, b, t) -> b = None) (snd cl.cl_context)) in
- let pars = fst (list_chop lenpars args) in
+ let pars = fst (List.chop lenpars args) in
match cl.cl_impl with
| IndRef ind -> Some (applistc (mkConstruct (ind, 1)) args),
applistc (mkInd ind) pars
| ConstRef cst ->
- let term = if args = [] then None else Some (list_last args) in
+ let term = if args = [] then None else Some (List.last args) in
term, applistc (mkConst cst) pars
| _ -> assert false
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index df1833f843..b24992b8d7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -100,7 +100,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
let e_type_case_branches env evdref (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 = e_is_correct_arity env evdref c pj ind specif params in
let lc = build_branches_type ind specif params p in
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-19 06:49:14 +0000