aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr_ops.ml2
-rw-r--r--interp/constrextern.ml18
-rw-r--r--interp/constrintern.ml40
-rw-r--r--interp/coqlib.ml4
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/modintern.ml2
-rw-r--r--interp/notation.ml10
-rw-r--r--interp/notation_ops.ml36
-rw-r--r--interp/reserve.ml2
-rw-r--r--interp/topconstr.ml2
11 files changed, 60 insertions, 60 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 950edc5a3..306fbfad9 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -75,7 +75,7 @@ let local_binder_loc = function
let local_binders_loc bll =
if bll = [] then Loc.ghost else
- Loc.merge (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
+ Loc.merge (local_binder_loc (List.hd bll)) (local_binder_loc (List.last bll))
(** Pseudo-constructors *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 272845d07..0ce8a8aac 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -257,7 +257,7 @@ let is_same_type c d =
(* mapping patterns to cases_pattern_expr *)
let add_patt_for_params ind l =
- Util.list_addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (Loc.ghost,None)) l
+ Util.List.addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (Loc.ghost,None)) l
let drop_implicits_in_patt cst nb_expl args =
let impl_st = (implicits_of_global cst) in
@@ -276,7 +276,7 @@ let drop_implicits_in_patt cst nb_expl args =
in
if nb_expl = 0 then aux impl_data
else
- let imps = list_skipn_at_least nb_expl (select_stronger_impargs impl_st) in
+ let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in
impls_fit [] (imps,args)
let has_curly_brackets ntn =
@@ -355,7 +355,7 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
let nb_params = Inductiveops.inductive_nparams ind in
List.exists (fun (_,impls) ->
(List.length impls >= nb_params) &&
- let params,args = Util.list_chop nb_params impls in
+ let params,args = Util.List.chop nb_params impls in
(List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args)
) impl_st
@@ -570,8 +570,8 @@ let explicitize loc inctx impl (cf,f) args =
let f' = match f with CRef f -> f | _ -> assert false in
CAppExpl (loc,(ip,f'),args)
else
- let (args1,args2) = list_chop i args in
- let (impl1,impl2) = if impl=[] then [],[] else list_chop i impl in
+ let (args1,args2) = List.chop i args in
+ let (impl1,impl2) = if impl=[] then [],[] else List.chop i impl in
let args1 = exprec 1 (args1,impl1) in
let args2 = exprec (i+1) (args2,impl2) in
CApp (loc,(Some (List.length args1),f),args1@args2)
@@ -617,7 +617,7 @@ let rec remove_coercions inctx = function
(try match Classops.hide_coercion r with
| Some n when n < nargs && (inctx or n+1 < nargs) ->
(* We skip a coercion *)
- let l = list_skipn n args in
+ let l = List.skipn n args in
let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
(* Recursively remove the head coercions *)
let a' = remove_coercions true a in
@@ -893,17 +893,17 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
let (t,args,argsscopes,argsimpls) = match t,n with
| GApp (_,f,args), Some n
when List.length args >= n ->
- let args1, args2 = list_chop n args in
+ let args1, args2 = List.chop n args in
let subscopes, impls =
match f with
| GRef (_,ref) ->
let subscopes =
- try list_skipn n (find_arguments_scope ref) with _ -> [] in
+ try List.skipn n (find_arguments_scope ref) with _ -> [] in
let impls =
let impls =
select_impargs_size
(List.length args) (implicits_of_global ref) in
- try list_skipn n impls with _ -> [] in
+ try List.skipn n impls with _ -> [] in
subscopes,impls
| _ ->
[], [] in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 86998c210..7ad1327fd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -193,7 +193,7 @@ let empty_internalization_env = Idmap.empty
let compute_explicitable_implicit imps = function
| Inductive params ->
(* In inductive types, the parameters are fixed implicit arguments *)
- let sub_impl,_ = list_chop (List.length params) imps in
+ let sub_impl,_ = List.chop (List.length params) imps in
let sub_impl' = List.filter is_status_implicit sub_impl in
List.map name_of_implicit sub_impl'
| Recursive | Method | Variable ->
@@ -206,7 +206,7 @@ let compute_internalization_data env ty typ impl =
(ty, expls_impl, impl, compute_arguments_scope typ)
let compute_internalization_env env ty =
- list_fold_left3
+ List.fold_left3
(fun map id typ impl -> Idmap.add id (compute_internalization_data env ty typ impl) map)
empty_internalization_env
@@ -674,7 +674,7 @@ let find_appl_head_data = function
when l <> [] & Flags.version_strictly_greater Flags.V8_2 ->
let n = List.length l in
x,List.map (drop_first_implicits n) (implicits_of_global ref),
- list_skipn_at_least n (find_arguments_scope ref),[]
+ List.skipn_at_least n (find_arguments_scope ref),[]
| x -> x,[],[],[]
let error_not_enough_arguments loc =
@@ -708,7 +708,7 @@ let intern_qualid loc qid intern env lvar args =
let (ids,c) = Syntax_def.search_syntactic_definition sp in
let nids = List.length ids in
if List.length args < nids then error_not_enough_arguments loc;
- let args1,args2 = list_chop nids args in
+ let args1,args2 = List.chop nids args in
check_no_explicitation args1;
let subst = make_subst ids (List.map fst args1) in
subst_aconstr_in_glob_constr loc intern lvar (subst,[],[]) ([],env) c, args2
@@ -766,15 +766,15 @@ let find_remaining_scopes pl1 pl2 ref =
let len_pl2 = List.length pl2 in
let impl_list = if len_pl1 = 0
then select_impargs_size len_pl2 impls_st
- else list_skipn_at_least len_pl1 (select_stronger_impargs impls_st) in
+ else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in
let allscs = find_arguments_scope ref in
- let scope_list = list_skipn_at_least len_pl1 allscs in
+ let scope_list = List.skipn_at_least len_pl1 allscs in
let rec aux = function
|[],l -> l
|_,[] -> []
|h::t,_::tt when is_status_implicit h -> aux (t,tt)
|_::t,h::tt -> h :: aux (t,tt)
- in ((try list_firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs),
+ in ((try List.firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs),
simple_adjust_scopes len_pl2 (aux (impl_list,scope_list)))
let product_of_cases_patterns ids idspl =
@@ -800,7 +800,7 @@ let rec has_duplicate = function
| x::l -> if List.mem x l then (Some x) else has_duplicate l
let loc_of_lhs lhs =
- Loc.merge (fst (List.hd lhs)) (fst (list_last lhs))
+ Loc.merge (fst (List.hd lhs)) (fst (List.last lhs))
let check_linearity lhs ids =
match has_duplicate ids with
@@ -815,7 +815,7 @@ let check_number_of_pattern loc n l =
if n<>p then raise (InternalizationError (loc,BadPatternsNumber (n,p)))
let check_or_pat_variables loc ids idsl =
- if List.exists (fun ids' -> not (list_eq_set ids ids')) idsl then
+ if List.exists (fun ids' -> not (List.eq_set ids ids')) idsl then
user_err_loc (loc, "", str
"The components of this disjunctive pattern must bind the same variables.")
@@ -832,7 +832,7 @@ let check_constructor_length env loc cstr len_pl pl0 =
let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 =
let impl_list = if len_pl1 = 0
then select_impargs_size (List.length pl2) impls_st
- else list_skipn_at_least len_pl1 (select_stronger_impargs impls_st) in
+ else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in
let remaining_args = List.fold_left (fun i x -> if is_status_implicit x then i else succ i) in
let rec aux i = function
|[],l -> let args_len = List.length l + List.length impl_list + len_pl1 in
@@ -870,7 +870,7 @@ let chop_params_pattern loc ind args with_letin =
then fst (Inductiveops.inductive_nargs ind)
else Inductiveops.inductive_nparams ind in
assert (nparams <= List.length args);
- let params,args = list_chop nparams args in
+ let params,args = List.chop nparams args in
List.iter (function PatVar(_,Anonymous) -> ()
| PatVar (loc',_) | PatCstr(loc',_,_,_) -> error_parameter_not_implicit loc') params;
args
@@ -883,7 +883,7 @@ let find_constructor loc add_params ref =
|Some nb_args -> let nb = if nb_args = Inductiveops.constructor_nrealhyps c
then fst (Inductiveops.inductive_nargs ind)
else Inductiveops.inductive_nparams ind in
- Util.list_make nb ([],[([],PatVar(Loc.ghost,Anonymous))])
+ Util.List.make nb ([],[([],PatVar(Loc.ghost,Anonymous))])
|None -> []) cstr
let find_pattern_variable = function
@@ -1033,7 +1033,7 @@ let drop_notations_pattern looked_for =
looked_for g;
let nvars = List.length vars in
if List.length pats < nvars then error_not_enough_arguments loc;
- let pats1,pats2 = list_chop nvars pats in
+ let pats1,pats2 = List.chop nvars pats in
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
let idspl1 = List.map (in_not loc env (subst,[]) []) args in
let (_,argscs) = find_remaining_scopes pats1 pats2 g in
@@ -1283,7 +1283,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
let dl = Array.of_list dl in
let n =
- try list_index0 iddef lf
+ try List.index0 iddef lf
with Not_found ->
raise (InternalizationError (locid,UnboundFixName (false,iddef)))
in
@@ -1308,7 +1308,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
in
((n, ro), List.rev rbl, intern_type env' ty, env')) dl in
let idl = array_map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
- let env'' = list_fold_left_i (fun i en name ->
+ let env'' = List.fold_left_i (fun i en name ->
let (_,bli,tyi,_) = idl_temp.(i) in
let fix_args = (List.map (fun (_,(na, bk, _, _)) -> (build_impls bk na)) bli) in
push_name_env lvar (impls_type_list ~args:fix_args tyi)
@@ -1324,7 +1324,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
let lf = List.map (fun ((_, id),_,_,_) -> id) dl in
let dl = Array.of_list dl in
let n =
- try list_index0 iddef lf
+ try List.index0 iddef lf
with Not_found ->
raise (InternalizationError (locid,UnboundFixName (true,iddef)))
in
@@ -1335,7 +1335,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
(List.rev rbl,
intern_type env' ty,env')) dl in
let idl = array_map2 (fun (_,_,_,bd) (b,c,env') ->
- let env'' = list_fold_left_i (fun i en name ->
+ let env'' = List.fold_left_i (fun i en name ->
let (bli,tyi,_) = idl_tmp.(i) in
let cofix_args = List.map (fun (_, (na, bk, _, _)) -> (build_impls bk na)) bli in
push_name_env lvar (impls_type_list ~args:cofix_args tyi)
@@ -1407,7 +1407,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
match cargs with
| None -> user_err_loc (loc, "intern", str"No constructor inference.")
| Some (n, constrname, args) ->
- let pars = list_make n (CHole (loc, None)) in
+ let pars = List.make n (CHole (loc, None)) in
let app = CAppExpl (loc, (None, constrname), List.rev_append pars args) in
intern env app
end
@@ -1440,7 +1440,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars, (* "match v1,..,vn" *)
[Loc.ghost,[],thepats, (* "|p1,..,pn" *)
Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType)) rtnpo; (* "=> P" is there were a P "=> _" else *)
- Loc.ghost,[],list_make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *)
+ Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *)
GHole(Loc.ghost,Evar_kinds.ImpossibleCase) (* "=> _" *)]))
in
let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
@@ -1553,7 +1553,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc)
|_ -> assert false in
let _,args_rel =
- list_chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
+ List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
canonize_args args_rel l (Idset.elements forbidden_names_for_gen) [] [] in
match_to_do, Some (cases_pattern_expr_loc t,ind,List.rev_map snd nal)
| None ->
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 94cb91749..531ca5bf4 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -45,7 +45,7 @@ let gen_constant_in_modules locstr dirs s =
let dirs = List.map make_dir dirs in
let qualid = qualid_of_string s in
let all = Nametab.locate_extended_all qualid in
- let all = list_uniquize (list_map_filter global_of_extended all) in
+ let all = List.uniquize (List.map_filter global_of_extended all) in
let these = List.filter (has_suffix_in_dirs dirs) all in
match these with
| [x] -> constr_of_global x
@@ -73,7 +73,7 @@ let check_required_library d =
if not (Library.library_is_loaded dir) then
if not current_dir then
(* Loading silently ...
- let m, prefix = list_sep_last d' in
+ let m, prefix = List.sep_last d' in
read_library
(Loc.ghost,make_qualid (make_dirpath (List.rev prefix)) m)
*)
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index c9e18c15e..101645dfc 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -174,7 +174,7 @@ let dump_constraint ((loc, n), _, _) sec ty =
let dump_modref loc mp ty =
if dump () then
let (dp, l) = Lib.split_modpath mp in
- let l = if l = [] then l else Util.list_drop_last l in
+ let l = if l = [] then l else Util.List.drop_last l in
let fp = Names.string_of_dirpath dp in
let mp = Names.string_of_dirpath (Names.make_dirpath l) in
let bl,el = interval loc in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 3057cef34..c4cc38a56 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -316,6 +316,6 @@ let implicits_of_glob_constr ?(with_products=true) l =
| GLetIn (loc, na, t, b) -> aux i b
| GRec (_, fix_kind, nas, args, tys, bds) ->
let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
- list_fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
+ List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
| _ -> []
in aux 1 l
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 1e7d84c96..ba5c68a5d 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -77,7 +77,7 @@ let lookup_qualid (modtype:bool) qid =
in
let rec find_module_prefix dir n =
if n<0 then raise Not_found;
- let dir',dir'' = list_chop n dir in
+ let dir',dir'' = List.chop n dir in
let id',dir''' =
match dir'' with
| hd::tl -> hd,tl
diff --git a/interp/notation.ml b/interp/notation.ml
index 6a574a56e..46a06b700 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -125,7 +125,7 @@ let open_scope i (_,(local,op,sc)) =
| _ -> sc
in
scope_stack :=
- if op then sc :: !scope_stack else list_except sc !scope_stack
+ if op then sc :: !scope_stack else List.except sc !scope_stack
let cache_scope o =
open_scope 1 o
@@ -285,7 +285,7 @@ let check_required_module loc sc (sp,d) =
with Not_found ->
user_err_loc (loc,"prim_token_interpreter",
str ("Cannot interpret in "^sc^" without requiring first module "
- ^(list_last d)^"."))
+ ^(List.last d)^"."))
(* Look if some notation or numeral printer in [scope] can be used in
the scope stack [scopes], and if yes, using delimiters or not *)
@@ -402,7 +402,7 @@ let interp_notation loc ntn local_scopes =
let isGApp = function GApp _ -> true | _ -> false
let uninterp_notations c =
- list_map_append (fun key -> Gmapl.find key !notations_key_table)
+ List.map_append (fun key -> Gmapl.find key !notations_key_table)
(glob_constr_keys c)
let uninterp_cases_pattern_notations c =
@@ -554,7 +554,7 @@ let subst_arguments_scope (subst,(req,r,scl,cls)) =
match subst_scope_class subst cl with
| Some cl' as ocl' when cl' != cl -> ocl'
| _ -> ocl in
- let cls' = list_smartmap subst_cl cls in
+ let cls' = List.smartmap subst_cl cls in
let scl' = merge_scope (List.map find_scope_class_opt cls') scl in
let scl'' = List.map (Option.map Declaremods.subst_scope) scl' in
(ArgsScopeNoDischarge,r',scl'',cls')
@@ -576,7 +576,7 @@ let rebuild_arguments_scope (req,r,l,_) =
(* Add to the manually given scopes the one found automatically
for the extra parameters of the section *)
let l',cls = compute_arguments_scope_full (Global.type_of_global r) in
- let l1,_ = list_chop (List.length l' - List.length l) l' in
+ let l1,_ = List.chop (List.length l' - List.length l) l' in
(req,r,l1@l,cls)
type arguments_scope_obj =
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index bd3ba4274..13356445f 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -33,7 +33,7 @@ let rec cases_pattern_fold_map loc g e = function
let e',na' = g e na in e', PatVar (loc,na')
| PatCstr (_,cstr,patl,na) ->
let e',na' = g e na in
- let e',patl' = list_fold_map (cases_pattern_fold_map loc g) e patl in
+ let e',patl' = List.fold_map (cases_pattern_fold_map loc g) e patl in
e', PatCstr (loc,cstr,patl',na')
let rec subst_glob_vars l = function
@@ -86,18 +86,18 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function
let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in
let eqnl' = List.map (fun (patl,rhs) ->
let ((idl,e),patl) =
- list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
+ List.fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
(loc,idl,patl,f e rhs)) eqnl in
GCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
| NLetTuple (nal,(na,po),b,c) ->
- let e',nal = list_fold_map g e nal in
+ let e',nal = List.fold_map g e nal in
let e'',na = g e na in
GLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c)
| NIf (c,(na,po),b1,b2) ->
let e',na = g e na in
GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2)
| NRec (fk,idl,dll,tl,bl) ->
- let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) ->
+ let e,dll = array_fold_map (List.fold_map (fun e (na,oc,b) ->
let e,na = g e na in
(e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
let e',idl = array_fold_map (to_id g) e idl in
@@ -144,7 +144,7 @@ let on_true_do b f c = if b then (f c; b) else b
let compare_glob_constr f add t1 t2 = match t1,t2 with
| GRef (_,r1), GRef (_,r2) -> eq_gr r1 r2
| GVar (_,v1), GVar (_,v2) -> on_true_do (v1 = v2) add (Name v1)
- | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 & list_for_all2eq f l1 l2
+ | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 & List.for_all2eq f l1 l2
| GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1
| GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
on_true_do (f ty1 ty2 & f c1 c2) add na1
@@ -182,7 +182,7 @@ let compare_recursive_parts found f (iterator,subc) =
(* We found the pattern, but there are extra arguments *)
(* (this allows e.g. alternative (recursive) notation of application) *)
assert (!terminator = None); terminator := Some term;
- list_for_all2eq aux l1 l2
+ List.for_all2eq aux l1 l2
| GVar (_,x), GVar (_,y) when x<>y ->
(* We found the position where it differs *)
let lassoc = (!terminator <> None) in
@@ -335,7 +335,7 @@ let rec subst_pat subst pat =
| PatVar _ -> pat
| PatCstr (loc,((kn,i),j),cpl,n) ->
let kn' = subst_ind subst kn
- and cpl' = list_smartmap (subst_pat subst) cpl in
+ and cpl' = List.smartmap (subst_pat subst) cpl in
if kn' == kn && cpl' == cpl then pat else
PatCstr (loc,((kn',i),j),cpl',n)
@@ -350,7 +350,7 @@ let rec subst_notation_constr subst bound raw =
| NApp (r,rl) ->
let r' = subst_notation_constr subst bound r
- and rl' = list_smartmap (subst_notation_constr subst bound) rl in
+ and rl' = List.smartmap (subst_notation_constr subst bound) rl in
if r' == r && rl' == rl then raw else
NApp(r',rl')
@@ -386,7 +386,7 @@ let rec subst_notation_constr subst bound raw =
| NCases (sty,rtntypopt,rl,branches) ->
let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt
- and rl' = list_smartmap
+ and rl' = List.smartmap
(fun (a,(n,signopt) as x) ->
let a' = subst_notation_constr subst bound a in
let signopt' = Option.map (fun ((indkn,i),nal as z) ->
@@ -394,9 +394,9 @@ let rec subst_notation_constr subst bound raw =
if indkn == indkn' then z else ((indkn',i),nal)) signopt in
if a' == a && signopt' == signopt then x else (a',(n,signopt')))
rl
- and branches' = list_smartmap
+ and branches' = List.smartmap
(fun (cpl,r as branch) ->
- let cpl' = list_smartmap (subst_pat subst) cpl
+ let cpl' = List.smartmap (subst_pat subst) cpl
and r' = subst_notation_constr subst bound r in
if cpl' == cpl && r' == r then branch else
(cpl',r'))
@@ -423,7 +423,7 @@ let rec subst_notation_constr subst bound raw =
| NRec (fk,idl,dll,tl,bl) ->
let dll' =
- array_smartmap (list_smartmap (fun (na,oc,b as x) ->
+ array_smartmap (List.smartmap (fun (na,oc,b as x) ->
let oc' = Option.smartmap (subst_notation_constr subst bound) oc in
let b' = subst_notation_constr subst bound b in
if oc' == oc && b' == b then x else (na,oc',b'))) dll in
@@ -619,9 +619,9 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
let n1 = List.length l1 and n2 = List.length l2 in
let f1,l1,f2,l2 =
if n1 < n2 then
- let l21,l22 = list_chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22
+ let l21,l22 = List.chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22
else if n1 > n2 then
- let l11,l12 = list_chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2
+ let l11,l12 = List.chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2
else f1,l1, f2, l2 in
let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in
List.fold_left2 (match_ may_use_eta u alp metas)
@@ -710,7 +710,7 @@ and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
match_in u alp metas sigma rhs1 rhs2
let match_notation_constr u c (metas,pat) =
- let vars = list_split_by (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in
+ let vars = List.split_by (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in
let vars = (List.map fst (fst vars), List.map fst (snd vars)) in
let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in
(* Reorder canonically the substitution *)
@@ -734,7 +734,7 @@ let match_notation_constr u c (metas,pat) =
let add_patterns_for_params ind l =
let mib,_ = Global.lookup_inductive ind in
let nparams = mib.Declarations.mind_nparams in
- Util.list_addn nparams (PatVar (Loc.ghost,Anonymous)) l
+ Util.List.addn nparams (PatVar (Loc.ghost,Anonymous)) l
let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
try
@@ -758,7 +758,7 @@ let rec match_cases_pattern metas sigma a1 a2 =
then
raise No_match
else
- let l1',more_args = Util.list_chop le2 l1 in
+ let l1',more_args = Util.List.chop le2 l1 in
(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
| r1, NList (x,_,iter,termin,lassoc) ->
(match_alist (fun (metas,_) -> match_cases_pattern_no_more_args metas)
@@ -781,7 +781,7 @@ let match_ind_pattern metas sigma ind pats a2 =
then
raise No_match
else
- let l1',more_args = Util.list_chop le2 pats in
+ let l1',more_args = Util.List.chop le2 pats in
(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
|_ -> raise No_match
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 259ffa171..7a2d4bfe7 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -77,7 +77,7 @@ let revert_reserved_type t =
try
let l = Gmapl.find (constr_key t) !reserve_revtable in
let t = Detyping.detype false [] [] t in
- list_try_find
+ List.try_find
(fun (pat,id) ->
try let _ = Notation_ops.match_notation_constr false t ([],pat) in Name id
with Notation_ops.No_match -> failwith "") l
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index e717e1747..abdde1f54 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -158,7 +158,7 @@ let split_at_annot bl na =
| Some (loc, id) ->
let rec aux acc = function
| LocalRawAssum (bls, k, t) as x :: rest ->
- let l, r = list_split_when (fun (loc, na) -> na = Name id) bls in
+ let l, r = List.split_when (fun (loc, na) -> na = Name id) bls in
if r = [] then aux (x :: acc) rest
else
(List.rev (if l = [] then acc else LocalRawAssum (l, k, t) :: acc),
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 20:11:06 +0000