diff options
Diffstat (limited to 'plugins')
29 files changed, 118 insertions, 118 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 53c146bfce..423c955094 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -367,7 +367,7 @@ let discriminate_tac cstr p gls = let build_term_to_complete uf meta pac = let cinfo = get_constructor_info uf pac.cnode in let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in - let dummy_args = List.rev (list_tabulate meta pac.arity) in + let dummy_args = List.rev (List.tabulate meta pac.arity) in let all_args = List.rev_append real_args dummy_args in applistc (mkConstruct cinfo.ci_constr) all_args diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 5e128bc423..f2f978ccdf 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -57,7 +57,7 @@ let intern_hyp iconstr globs = function Hprop (intern_statement iconstr globs st) let intern_hyps iconstr globs hyps = - snd (list_fold_map (intern_hyp iconstr) globs hyps) + snd (List.fold_map (intern_hyp iconstr) globs hyps) let intern_cut intern_it globs cut= let nglobs,nstat=intern_it globs cut.cut_stat in @@ -74,10 +74,10 @@ let intern_hyp_list args globs = let intern_one globs (loc,(id,opttyp)) = (add_var id globs), (loc,(id,Option.map (intern_constr globs) opttyp)) in - list_fold_map intern_one globs args + List.fold_map intern_one globs args let intern_suffices_clause globs (hyps,c) = - let nglobs,nhyps = list_fold_map (intern_hyp intern_constr) globs hyps in + let nglobs,nhyps = List.fold_map (intern_hyp intern_constr) globs hyps in nglobs,(nhyps,intern_constr_or_thesis nglobs c) let intern_fundecl args body globs= @@ -340,7 +340,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = (fun (loc,(id,_)) -> GVar (loc,id)) params in let dum_args= - list_tabulate + List.tabulate (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false))) oib.Declarations.mind_nrealargs in glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 31e15081b2..1a0d05047e 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -857,7 +857,7 @@ let build_per_info etype casee gls = match etype with ET_Induction -> mind.mind_nparams_rec,Some (snd ind) | _ -> mind.mind_nparams,None in - let params,real_args = list_chop nparams args in + let params,real_args = List.chop nparams args in let abstract_obj c body = let typ=pf_type_of gls c in lambda_create env (typ,subst_term c body) in @@ -953,7 +953,7 @@ let rec tree_of_pats ((id,_) as cpl) pats = let nexti i ati = if i = pred cnum then let nargs = - list_map_i (fun j a -> (a,ati.(j))) 0 args in + List.map_i (fun j a -> (a,ati.(j))) 0 args in Some (Idset.singleton id, tree_of_pats cpl (nargs::rest_args::stack)) else None @@ -998,7 +998,7 @@ let rec add_branch ((id,_) as cpl) pats tree= let nexti i ati = if i = pred cnum then let nargs = - list_map_i (fun j a -> (a,ati.(j))) 0 args in + List.map_i (fun j a -> (a,ati.(j))) 0 args in Some (Idset.add id ids, add_branch cpl (nargs::rest_args::stack) (skip_args t ids (Array.length ati))) @@ -1013,7 +1013,7 @@ let rec add_branch ((id,_) as cpl) pats tree= let mapi i ati bri = if i = pred cnum then let nargs = - list_map_i (fun j a -> (a,ati.(j))) 0 args in + List.map_i (fun j a -> (a,ati.(j))) 0 args in append_branch cpl 0 (nargs::rest_args::stack) bri else bri in @@ -1051,7 +1051,7 @@ let thesis_for obj typ per_info env= errorlabstrm "thesis_for" ((Printer.pr_constr_env env obj) ++ spc () ++ str"cannot give an induction hypothesis (wrong inductive type).") in - let params,args = list_chop per_info.per_nparams all_args in + let params,args = List.chop per_info.per_nparams all_args in let _ = if not (List.for_all2 eq_constr params per_info.per_params) then errorlabstrm "thesis_for" ((Printer.pr_constr_env env obj) ++ spc () ++ @@ -1182,7 +1182,7 @@ let hrec_for fix_id per_info gls obj_id = let rc,hd1=decompose_prod typ in let cind,all_args=decompose_app typ in let ind = destInd cind in assert (ind=per_info.per_ind); - let params,args= list_chop per_info.per_nparams all_args in + let params,args= List.chop per_info.per_nparams all_args in assert begin try List.for_all2 eq_constr params per_info.per_params with Invalid_argument _ -> false end; @@ -1203,8 +1203,8 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = match List.assoc id args with [None,br_args] -> let all_metas = - list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps) in - let param_metas,hyp_metas = list_chop nparams all_metas in + List.tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps) in + let param_metas,hyp_metas = List.chop nparams all_metas in tclTHEN (tclDO nhrec introf) (tacnext @@ -1221,7 +1221,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let ctyp=pf_type_of gls casee in let hd,all_args = decompose_app (special_whd gls ctyp) in let _ = assert (destInd hd = ind) in (* just in case *) - let params,real_args = list_chop nparams all_args in + let params,real_args = List.chop nparams all_args in let abstract_obj c body = let typ=pf_type_of gls c in lambda_create env (typ,subst_term c body) in diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index b6b7e58338..8cceb2a111 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -349,7 +349,7 @@ let rec mp_renaming_fun mp = match mp with | MPfile _ -> assert (modular ()); (* see [at_toplevel] above *) assert (get_phase () = Pre); - let current_mpfile = (list_last (get_visible ())).mp in + let current_mpfile = (List.last (get_visible ())).mp in if mp <> current_mpfile then mpfiles_add mp; [string_of_modfile mp] @@ -496,7 +496,7 @@ let fstlev_ks k = function let pp_ocaml_local k prefix mp rls olab = (* what is the largest prefix of [mp] that belongs to [visible]? *) assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *) - let rls' = list_skipn (mp_length prefix) rls in + let rls' = List.skipn (mp_length prefix) rls in let k's = fstlev_ks k rls' in (* Reference r / module path mp is of the form [<prefix>.s.<...>]. *) if not (visible_clash prefix k's) then dottify rls' diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 588fe0cf23..b5cdec3ece 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -150,9 +150,9 @@ let factor_fix env l cb msb = if n = 1 then [|l|], recd, msb else begin if List.length msb < n-1 then raise Impossible; - let msb', msb'' = list_chop (n-1) msb in + let msb', msb'' = List.chop (n-1) msb in let labels = Array.make n l in - list_iter_i + List.iter_i (fun j -> function | (l,SFBconst cb') -> @@ -207,7 +207,7 @@ let env_for_mtb_with_def env mp seb idl = in let l = label_of_id (List.hd idl) in let spot = function (l',SFBconst _) -> l = l' | _ -> false in - let before = fst (list_split_when spot sig_b) in + let before = fst (List.split_when spot sig_b) in Modops.add_signature mp before empty_delta_resolver env (* From a [structure_body] (i.e. a list of [structure_field_body]) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0556f6d77f..e1bbcf9c75 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -193,7 +193,7 @@ let parse_ind_args si args relmax = let oib_equal o1 o2 = id_ord o1.mind_typename o2.mind_typename = 0 && - list_equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt && + List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt && begin match o1.mind_arity, o2.mind_arity with | Monomorphic {mind_user_arity=c1; mind_sort=s1}, Monomorphic {mind_user_arity=c2; mind_sort=s2} -> @@ -206,10 +206,10 @@ let mib_equal m1 m2 = m1.mind_record = m2.mind_record && m1.mind_finite = m2.mind_finite && m1.mind_ntypes = m2.mind_ntypes && - list_equal eq_named_declaration m1.mind_hyps m2.mind_hyps && + List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps && m1.mind_nparams = m2.mind_nparams && m1.mind_nparams_rec = m2.mind_nparams_rec && - list_equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt && + List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt && m1.mind_constraints = m2.mind_constraints (*S Extraction of a type. *) @@ -439,7 +439,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) | _ -> [] in let field_names = - list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in + List.skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in assert (List.length field_names = List.length typ); let projs = ref Cset.empty in let mp,d,_ = repr_mind kn in @@ -674,7 +674,7 @@ and extract_cst_app env mle mlt kn args = let mla = if not magic1 then try - let l,l' = list_chop (projection_arity (ConstRef kn)) mla in + let l,l' = List.chop (projection_arity (ConstRef kn)) mla in if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l' else mla with _ -> mla @@ -697,7 +697,7 @@ and extract_cst_app env mle mlt kn args = (* Partially applied function with some logical arg missing. We complete via eta and expunge logical args. *) let ls' = ls-la in - let s' = list_skipn la s in + let s' = List.skipn la s in let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in let e = anonym_or_dummy_lams (mlapp head mla) s' in put_magic_if magic2 (remove_n_lams (List.length optdummy) e) @@ -729,7 +729,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = let la = List.length args in assert (la <= ls + params_nb); let la' = max 0 (la - params_nb) in - let args' = list_lastn la' args in + let args' = List.lastn la' args in (* Now, we build the expected type of the constructor *) let metas = List.map new_meta args' in (* If stored and expected types differ, then magic! *) @@ -758,7 +758,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = then put_magic_if (magic2 && not magic1) (head mla) else (* [ params_nb <= la <= ls + params_nb ] *) let ls' = params_nb + ls - la in - let s' = list_lastn ls' s in + let s' = List.lastn ls' s in let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in put_magic_if magic2 (anonym_or_dummy_lams (head mla) s') @@ -847,7 +847,7 @@ let decomp_lams_eta_n n m env c t = let rels',c = decompose_lam c in let d = n - m in (* we'd better keep rels' as long as possible. *) - let rels = (list_firstn d rels) @ rels' in + let rels = (List.firstn d rels) @ rels' in let eta_args = List.rev_map mkRel (interval 1 d) in rels, applist (lift d c,eta_args) @@ -886,7 +886,7 @@ let extract_std_constant env kn body typ = and m = nb_lam body in if n <= m then decompose_lam_n n body else - let s,s' = list_chop m s in + let s,s' = List.chop m s in if List.for_all ((=) Keep) s' && (lang () = Haskell || sign_kind s <> UnsafeLogicalSig) then decompose_lam_n m body @@ -895,7 +895,7 @@ let extract_std_constant env kn body typ = (* Should we do one eta-expansion to avoid non-generalizable '_a ? *) let rels, c = let n = List.length rels in - let s,s' = list_chop n s in + let s,s' = List.chop n s in let k = sign_kind s in let empty_s = (k = EmptySig || k = SafeLogicalSig) in if lang () = Ocaml && empty_s && not (gentypvar_ok c) @@ -904,8 +904,8 @@ let extract_std_constant env kn body typ = else rels,c in let n = List.length rels in - let s = list_firstn n s in - let l,l' = list_chop n l in + let s = List.firstn n s in + let l,l' = List.chop n l in let t' = type_recomp (l',t') in (* The initial ML environment. *) let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 3b89386d40..3716695b86 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -534,7 +534,7 @@ let is_regular_match br = match pat with | Pusual r -> r | Pcons (r,l) -> - if not (list_for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l)) + if not (List.for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l)) then raise Impossible; r | _ -> raise Impossible @@ -636,9 +636,9 @@ let eta_red e = if m = n then [], f, a else if m < n then - list_skipn m ids, f, a + List.skipn m ids, f, a else (* m > n *) - let a1,a2 = list_chop (m-n) a in + let a1,a2 = List.chop (m-n) a in [], MLapp (f,a1), a2 in let p = List.length args in @@ -969,7 +969,7 @@ and simpl_case o typ br e = else ([], Pwild, ast_pop f) in let brl = Array.to_list br in - let brl_opt = list_filter_i (fun i _ -> not (Intset.mem i ints)) brl in + let brl_opt = List.filter_i (fun i _ -> not (Intset.mem i ints)) brl in let brl_opt = brl_opt @ [last_br] in MLcase (typ, e, Array.of_list brl_opt) | None -> MLcase (typ, e, br) @@ -1022,8 +1022,8 @@ let kill_dummy_lams c = | Keep :: bl -> fst_kill (n+1) bl in let skip = max 0 ((fst_kill 0 bl) - 1) in - let ids_skip, ids = list_chop skip ids in - let _, bl = list_chop skip bl in + let ids_skip, ids = List.chop skip ids in + let _, bl = List.chop skip bl in let c = named_lams ids_skip c in let ids',c = kill_some_lams bl (ids,c) in ids, named_lams ids' c @@ -1051,7 +1051,7 @@ let case_expunge s e = let m = List.length s in let n = nb_lams e in let p = if m <= n then collect_n_lams m e - else eta_expansion_sign (list_skipn n s) (collect_lams e) in + else eta_expansion_sign (List.skipn n s) (collect_lams e) in kill_some_lams (List.rev s) p (*s [term_expunge] takes a function [fun idn ... id1 -> c] @@ -1085,7 +1085,7 @@ let kill_dummy_args ids r t = let a = List.map (killrec n) a in let a = List.map (ast_lift k) a in let a = select_via_bl bl (a @ (eta_args k)) in - named_lams (list_firstn k ids) (MLapp (ast_lift k e, a)) + named_lams (List.firstn k ids) (MLapp (ast_lift k e, a)) | e when found n e -> let a = select_via_bl bl (eta_args m) in named_lams ids (MLapp (ast_lift m e, a)) @@ -1164,7 +1164,7 @@ let general_optimize_fix f ids n args m c = | MLrel j when v.(j-1)>=0 -> if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1) | _ -> raise Impossible - in list_iter_i aux args; + in List.iter_i aux args; let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in let new_f = anonym_tmp_lams (MLapp (MLrel (n+m+1),args_f)) m in let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 1211bbf173..8659de03eb 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -30,7 +30,7 @@ let se_iter do_decl do_spec = | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt' | MTwith (mt,ML_With_type(idl,l,t))-> let mp_mt = msid_of_mt mt in - let l',idl' = list_sep_last idl in + let l',idl' = List.sep_last idl in let mp_w = List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl' in diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 34ae1f9ad8..951049b7b2 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -114,7 +114,7 @@ let pp_one_field r i = function let pp_field r fields i = pp_one_field r i (List.nth fields i) -let pp_fields r fields = list_map_i (pp_one_field r) 0 fields +let pp_fields r fields = List.map_i (pp_one_field r) 0 fields (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses are needed or not. *) @@ -189,7 +189,7 @@ let rec pp_expr par env args = hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2)) | MLglob r -> (try - let args = list_skipn (projection_arity r) args in + let args = List.skipn (projection_arity r) args in let record = List.hd args in pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) with _ -> apply (pp_global Term r)) @@ -642,7 +642,7 @@ and pp_module_type params = function | MTwith(mt,ML_With_type(idl,vl,typ)) -> let ids = pp_parameters (rename_tvars keywords vl) in let mp_mt = msid_of_mt mt in - let l,idl' = list_sep_last idl in + let l,idl' = List.sep_last idl in let mp_w = List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl' in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 2dd07b2f2b..6151abf6eb 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -671,7 +671,7 @@ let add_implicits r l = else err (int i ++ str " is not a valid argument number for " ++ safe_pr_global r) | ArgId id -> - (try list_index (Name id) names + (try List.index (Name id) names with Not_found -> err (str "No argument " ++ pr_id id ++ str " for " ++ safe_pr_global r)) @@ -877,7 +877,7 @@ let extract_inductive r s l optstr = Lib.add_anonymous_leaf (in_customs (g,[],s)); Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s))) optstr; - list_iter_i + List.iter_i (fun j s -> let g = ConstructRef (ip,succ j) in Lib.add_anonymous_leaf (inline_extraction (true,[g])); diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 7abb4dc527..f4cc397bcc 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -142,7 +142,7 @@ let build_atoms gl metagen side cciterm = let g i _ (_,_,t) = build_rec env polarity (lift i t) in let f l = - list_fold_left_i g (1-(List.length l)) () l in + List.fold_left_i g (1-(List.length l)) () l in if polarity && (* we have a constant constructor *) array_exists (function []->true|_->false) v then trivial:=true; @@ -152,7 +152,7 @@ let build_atoms gl metagen side cciterm = let v =(ind_hyps 1 i l gl).(0) in let g i _ (_,_,t) = build_rec (var::env) polarity (lift i t) in - list_fold_left_i g (2-(List.length l)) () v + List.fold_left_i g (2-(List.length l)) () v | Forall(_,b)-> let var=mkMeta (metagen true) in build_rec (var::env) polarity b @@ -224,7 +224,7 @@ let build_formula side nam typ gl metagen= | And(_,_,_) -> Rand | Or(_,_,_) -> Ror | Exists (i,l) -> - let (_,_,d)=list_last (ind_hyps 0 i l gl).(0) in + let (_,_,d)=List.last (ind_hyps 0 i l gl).(0) in Rexists(m,d,trivial) | Forall (_,a) -> Rforall | Arrow (a,b) -> Rarrow in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index e3367b4c22..414afad467 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -112,7 +112,7 @@ let mk_open_instance id gl m t= match nam with Name id -> id | Anonymous -> dummy_bvid in - let revt=substl (list_tabulate (fun i->mkRel (m-i)) m) t in + let revt=substl (List.tabulate (fun i->mkRel (m-i)) m) t in let rec aux n avoid= if n=0 then [] else let nid=(fresh_id avoid var_id gl) in diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 37d9edef86..7acabaaa4c 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -129,7 +129,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl= let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in it_mkLambda_or_LetIn head rc in let lp=Array.length rcs in - let newhyps=list_tabulate myterm lp in + let newhyps=List.tabulate myterm lp in tclIFTHENELSE (tclTHENLIST [generalize newhyps; diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 6d00e8d9fb..c648939bb0 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -191,9 +191,9 @@ let empty_seq depth= depth=depth} let expand_constructor_hints = - list_map_append (function + List.map_append (function | IndRef ind -> - list_tabulate (fun i -> ConstructRef (ind,i+1)) + List.tabulate (fun i -> ConstructRef (ind,i+1)) (Inductiveops.nconstructors ind) | gr -> [gr]) diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 33ea0ac8a0..c3726f1a83 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -124,7 +124,7 @@ let unif_atoms i dom t1 t2= | Not_found ->Some (Phantom dom) let renum_metas_from k n t= (* requires n = max (free_rels t) *) - let l=list_tabulate (fun i->mkMeta (k+i)) n in + let l=List.tabulate (fun i->mkMeta (k+i)) n in substl l t let more_general (m1,t1) (m2,t2)= diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8ea4be631c..0796930fca 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -93,7 +93,7 @@ let observe_tac s = observe_tac_stream (str s) let list_chop ?(msg="") n l = try - list_chop n l + List.chop n l with Failure (msg') -> failwith (msg ^ msg') @@ -319,7 +319,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = ) in let new_type_of_hyp,ctxt_size,witness_fun = - list_fold_left_i + List.fold_left_i (fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) -> try let witness = Intmap.find i sub in @@ -1168,7 +1168,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : typess in let pte_to_fix,rev_info = - list_fold_left_i + List.fold_left_i (fun i (acc_map,acc_info) (pte,_,_) -> let infos = info_array.(i) in let type_args,_ = decompose_prod infos.types in @@ -1557,7 +1557,7 @@ let prove_principle_for_gen (* str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *) (* str "npost_rec_arg := " ++ int npost_rec_arg ); *) let (post_rec_arg,pre_rec_arg) = - Util.list_chop npost_rec_arg princ_info.args + Util.List.chop npost_rec_arg princ_info.args in let rec_arg_id = match List.rev post_rec_arg with @@ -1624,7 +1624,7 @@ let prove_principle_for_gen Elim.h_decompose_and (mkVar hid); (fun g -> let new_hyps = pf_ids_of_hyps g in - tcc_list := List.rev (list_subtract new_hyps (hid::hyps)); + tcc_list := List.rev (List.subtract new_hyps (hid::hyps)); if !tcc_list = [] then begin diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index e2dc149b09..f2eb4b23cf 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -88,7 +88,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = Nameops.out_name x,None,compose_prod real_args (mkSort new_sort) in let new_predicates = - list_map_i + List.map_i change_predicate_sort 0 princ_type_info.predicates @@ -252,7 +252,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in let pre_res = replace_vars - (list_map_i (fun i id -> (id, mkRel i)) 1 ptes_vars) + (List.map_i (fun i id -> (id, mkRel i)) 1 ptes_vars) (lift (List.length ptes_vars) pre_res) in it_mkProd_or_LetIn @@ -460,7 +460,7 @@ let get_funs_constant mp dp = let first_params = List.hd l_params in List.iter (fun params -> - if not (list_equal (fun (n1, c1) (n2, c2) -> n1 = n2 && eq_constr c1 c2) first_params params) + if not (List.equal (fun (n1, c1) (n2, c2) -> n1 = n2 && eq_constr c1 c2) first_params params) then error "Not a mutal recursive block" ) l_params diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index d11c01672a..1c21934495 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -89,7 +89,7 @@ let combine_results in (* and then we flatten the map *) { result = List.concat pre_result; - to_avoid = list_union res1.to_avoid res2.to_avoid + to_avoid = List.union res1.to_avoid res2.to_avoid } @@ -269,7 +269,7 @@ let make_discr_match_el = end *) let make_discr_match_brl i = - list_map_i + List.map_i (fun j (_,idl,patl,_) -> if j=i then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref)) @@ -659,7 +659,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let case_pats = build_constructors_of_type ind [] in assert (Array.length case_pats = 2); let brl = - list_map_i + List.map_i (fun i x -> (Loc.ghost,[],[case_pats.(i)],x)) 0 [lhs;rhs] @@ -748,7 +748,7 @@ and build_entry_lc_from_case env funname make_discr { result = List.concat (List.map (fun r -> r.result) results); to_avoid = - List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results + List.fold_left (fun acc r -> List.union acc r.to_avoid) [] results } and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid @@ -818,7 +818,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve let those_pattern_preconds = (List.flatten ( - list_map3 + List.map3 (fun pat e typ_as_constr -> let this_pat_ids = ids_of_pat pat in let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr in @@ -977,7 +977,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let mib,_ = Global.lookup_inductive ind in let nparam = mib.Declarations.mind_nparams in let params,arg' = - ((Util.list_chop nparam args')) + ((Util.List.chop nparam args')) in let rt_typ = GApp(Loc.ghost, @@ -1000,7 +1000,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match kind_of_term eq'_as_constr with | App(_,[|_;_;ty;_|]) -> let ty = Array.to_list (snd (destApp ty)) in - let ty' = snd (Util.list_chop nparam ty) in + let ty' = snd (Util.List.chop nparam ty) in List.fold_left2 (fun acc var_as_constr arg -> if isRel var_as_constr @@ -1238,7 +1238,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b let l = ref [] in let _ = try - list_iter_i + List.iter_i (fun i ((n,nt,is_defined) as param) -> if array_for_all (fun l -> @@ -1362,7 +1362,7 @@ let do_build_inductive in let rel_arity i funargs = (* Reduilding arities (with parameters) *) let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list = - (snd (list_chop nrel_params funargs)) + (snd (List.chop nrel_params funargs)) in List.fold_right (fun (n,t,is_defined) acc -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 52562fb374..18b2bbe2f7 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -21,7 +21,7 @@ let is_rec_info scheme_info = Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br ) in - Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches) + Util.List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches) let choose_dest_or_ind scheme_info = if is_rec_info scheme_info @@ -337,7 +337,7 @@ let generate_principle on_error in let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in let _ = - list_map_i + List.map_i (fun i x -> let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in let princ_type = Typeops.type_of_constant (Global.env()) princ @@ -392,7 +392,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas if List.length names = 1 then 1 else error "Recursive argument must be specified" | Some wf_arg -> - list_index (Name wf_arg) names + List.index (Name wf_arg) names in let unbounded_eq = let f_app_args = @@ -516,7 +516,7 @@ let decompose_lambda_n_assum_constr_expr = (n - nal_length) (Constrexpr.CLambdaN(lambda_loc,bl,e')) else - let nal_keep,nal_expr = list_chop n nal in + let nal_keep,nal_expr = List.chop n nal in (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc), Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e') ) @@ -548,7 +548,7 @@ let decompose_prod_n_assum_constr_expr = (if bl = [] then e' else (Constrexpr.CLambdaN(lambda_loc,bl,e'))) else (* let _ = Pp.msgnl (str "second case") in *) - let nal_keep,nal_expr = list_chop n nal in + let nal_keep,nal_expr = List.chop n nal in (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc), Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e') ) @@ -585,7 +585,7 @@ let rec rebuild_bl (aux,assoc) bl typ = let lnal' = List.length nal' in if lnal' >= lnal then - let old_nal',new_nal' = list_chop lnal nal' in + let old_nal',new_nal' = List.chop lnal nal' in rebuild_bl ((LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't)::aux),(make_assoc assoc old_nal' nal)) bl' (if new_nal' = [] && rest = [] then typ' @@ -593,7 +593,7 @@ let rec rebuild_bl (aux,assoc) bl typ = then CProdN(Loc.ghost,rest,typ') else CProdN(Loc.ghost,((new_nal',bk',nal't)::rest),typ')) else - let captured_nal,non_captured_nal = list_chop lnal' nal in + let captured_nal,non_captured_nal = List.chop lnal' nal in rebuild_nal ((LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't)::aux), (make_assoc assoc nal' captured_nal)) bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ')) | _ -> assert false @@ -789,7 +789,7 @@ let rec chop_n_arrow n t = else let new_t' = Constrexpr.CProdN(Loc.ghost, - ((snd (list_chop n nal)),k,t'')::nal_ta',t') + ((snd (List.chop n nal)),k,t'')::nal_ta',t') in raise (Stop new_t') in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 2f6a6a7d7b..1d1089a549 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -370,7 +370,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem in (* in fact we must also add the parameters to the constructor args *) let constructor_args g = - let params_id = fst (list_chop princ_infos.nparams args_names) in + let params_id = fst (List.chop princ_infos.nparams args_names) in (List.map mkVar params_id)@((constructor_args g)) in (* We then get the constructor corresponding to this branch and @@ -446,7 +446,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem ) lemmas_types_infos in - let param_names = fst (list_chop princ_infos.nparams args_names) in + let param_names = fst (List.chop princ_infos.nparams args_names) in let params = List.map mkVar param_names in let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in (* The bindings of the principle @@ -611,7 +611,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem in (* in fact we must also add the parameters to the constructor args *) let constructor_args = - let params_id = fst (list_chop princ_infos.nparams args_names) in + let params_id = fst (List.chop princ_infos.nparams args_names) in (List.map mkVar params_id)@(List.rev constructor_args) in (* We then get the constructor corresponding to this branch and @@ -669,7 +669,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem g in (* end of branche proof *) - let param_names = fst (list_chop princ_infos.nparams args_names) in + let param_names = fst (List.chop princ_infos.nparams args_names) in let params = List.map mkVar param_names in let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in (* The bindings of the principle @@ -996,7 +996,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = ] g in - let params_names = fst (list_chop princ_infos.nparams args_names) in + let params_names = fst (List.chop princ_infos.nparams args_names) in let params = List.map mkVar params_names in tclTHENSEQ [ tclMAP h_intro (args_names@[res;hres]); diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 4fe22a3543..21c0d86a4f 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -165,11 +165,11 @@ let array_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b array): 'a = let res = f !i acc x in i := !i + 1; res) acc arr -(* Like list_chop but except that [i] is the size of the suffix of [l]. *) +(* Like List.chop but except that [i] is the size of the suffix of [l]. *) let list_chop_end i l = let size_prefix = List.length l -i in if size_prefix < 0 then failwith "list_chop_end" - else list_chop size_prefix l + else List.chop size_prefix l let list_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b list): 'a = let i = ref 0 in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 14d9b7fcb0..8b0fc27397 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -705,7 +705,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = (try (tclTHENS destruct_tac - (list_map_i (fun i e -> observe_tac (str "do treat case") (treat_case b to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l) + (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case b to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l) )) with | UserError("Refiner.thensn_tac3",_) @@ -1014,7 +1014,7 @@ let compute_terminate_type nb_args func = Array.of_list (lift 5 a_arrow_b:: mkRel 3:: constr_of_global func::mkRel 1:: - List.rev (list_map_i (fun i _ -> mkRel (6+i)) 0 rev_args) + List.rev (List.map_i (fun i _ -> mkRel (6+i)) 0 rev_args) ) ) in @@ -1044,7 +1044,7 @@ let termination_proof_header is_mes input_type ids args_id relation let nargs = List.length args_id in let pre_rec_args = List.rev_map - mkVar (fst (list_chop (rec_arg_num - 1) args_id)) + mkVar (fst (List.chop (rec_arg_num - 1) args_id)) in let relation = substl pre_rec_args relation in let input_type = substl pre_rec_args input_type in @@ -1297,7 +1297,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ (Elim.h_decompose_and (mkVar hid)) (fun g -> let ids' = pf_ids_of_hyps g in - lid := List.rev (list_subtract ids' ids); + lid := List.rev (List.subtract ids' ids); if !lid = [] then lid := [hid]; tclIDTAC g ) diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index e0b27a2f59..94b79503af 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -214,7 +214,7 @@ let ppcm_mon m m' = let repr p = p let equal = - Util.list_for_all2eq + Util.List.for_all2eq (fun (c1,m1) (c2,m2) -> P.equal c1 c2 && m1=m2) let hash p = diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index ed06d6e118..ccf397eda2 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -153,7 +153,7 @@ let tag_hypothesis,tag_of_hyp, hyp_of_tag = let hide_constr,find_constr,clear_tables,dump_tables = let l = ref ([]:(constr * (identifier * identifier * bool)) list) in (fun h id eg b -> l := (h,(id,eg,b)):: !l), - (fun h -> try list_assoc_f eq_constr h !l with Not_found -> failwith "find_contr"), + (fun h -> try List.assoc_f eq_constr h !l with Not_found -> failwith "find_contr"), (fun () -> l := []), (fun () -> !l) diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 62c0dc4a9c..ee341cbc28 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -26,7 +26,7 @@ let omega_tactic l = | "N" -> Tacinterp.interp <:tactic<zify_N>> | "Z" -> Tacinterp.interp <:tactic<zify_op>> | s -> Errors.error ("No Omega knowledge base for type "^s)) - (Util.list_uniquize (List.sort compare l)) + (Util.List.uniquize (List.sort compare l)) in tclTHEN (tclREPEAT (tclPROGRESS (tclTHENLIST tacs))) diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index 98cad09e02..6abcc7b6f7 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -352,11 +352,11 @@ let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = let new_eq = List.hd (normalize new_eq) in let eliminated_var, def = chop_var var new_eq.body in let other_equations = - Util.list_map_append + Util.List.map_append (fun e -> normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l1 in let inequations = - Util.list_map_append + Util.List.map_append (fun e -> normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l2 in let original' = eliminate_with_in new_eq_id eliminated_var new_eq original in @@ -368,9 +368,9 @@ let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e, if !debug then display_system print_var (e::other); try let v,def = chop_factor_1 e.body in - (Util.list_map_append + (Util.List.map_append (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) other, - Util.list_map_append + Util.List.map_append (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) ineqs) with FACTOR1 -> eliminate_one_equation new_ids (banerjee_step new_ids e other ineqs) @@ -523,7 +523,7 @@ let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system = failwith "disequation in simplify"; clear_history (); List.iter (fun e -> add_event (HYP e)) system; - let system = Util.list_map_append normalize system in + let system = Util.List.map_append normalize system in let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in let system = (eqs @ simp_eq,simp_ineq) in @@ -658,7 +658,7 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = | ([],ineqs,expl_map) -> ineqs,expl_map in try - let system = Util.list_map_append normalize system in + let system = Util.List.map_append normalize system in let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in let dise,ine = List.partition (fun e -> e.kind = DISE) ineqs in let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in @@ -700,13 +700,13 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = let s1,s2 = List.partition (fun (_,_,decomp,_) -> sign decomp) systems in let s1' = - List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s1 in + List.map (fun (dep,ro,dc,pa) -> (Util.List.except id dep,ro,dc,pa)) s1 in let s2' = - List.map (fun (dep,ro,dc,pa) -> (Util.list_except id dep,ro,dc,pa)) s2 in + List.map (fun (dep,ro,dc,pa) -> (Util.List.except id dep,ro,dc,pa)) s2 in let (r1,relie1) = solve s1' and (r2,relie2) = solve s2' in let (eq,id1,id2) = List.assoc id explode_map in - [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.list_union relie1 relie2 + [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.List.union relie1 relie2 with FULL_SOLUTION (x0,x1) -> (x0,x1) in let act,relie_on = solve all_solutions in diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index a548d4d4a7..5a843e2b76 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -19,7 +19,7 @@ let romega_tactic l = | "N" -> Tacinterp.interp <:tactic<zify_N>> | "Z" -> Tacinterp.interp <:tactic<zify_op>> | s -> Errors.error ("No ROmega knowledge base for type "^s)) - (Util.list_uniquize (List.sort compare l)) + (Util.List.uniquize (List.sort compare l)) in tclTHEN (tclREPEAT (tclPROGRESS (tclTHENLIST tacs))) diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 50031052ba..6c6e2c57f2 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -220,7 +220,7 @@ let unintern_omega env id = calcul des variables utiles. *) let add_reified_atom t env = - try list_index0_f Term.eq_constr t env.terms + try List.index0_f Term.eq_constr t env.terms with Not_found -> let i = List.length env.terms in env.terms <- env.terms @ [t]; i @@ -231,7 +231,7 @@ let get_reified_atom env = (* \subsection{Gestion de l'environnement de proposition pour Omega} *) (* ajout d'une proposition *) let add_prop env t = - try list_index0_f Term.eq_constr t env.props + try List.index0_f Term.eq_constr t env.props with Not_found -> let i = List.length env.props in env.props <- env.props @ [t]; i @@ -412,7 +412,7 @@ pour faire des opérations de normalisation sur les équations. *) (* Extraction des variables d'une équation. *) (* Chaque fonction retourne une liste triée sans redondance *) -let (@@) = list_merge_uniq compare +let (@@) = List.merge_uniq compare let rec vars_of_formula = function | Oint _ -> [] @@ -812,7 +812,7 @@ let destructurate_hyps syst = (i,t) :: l -> let l_syst1 = destructurate_pos_hyp i [] [] t in let l_syst2 = loop l in - list_cartesian (@) l_syst1 l_syst2 + List.cartesian (@) l_syst1 l_syst2 | [] -> [[]] in loop syst @@ -912,13 +912,13 @@ let add_stated_equations env tree = (* PL: experimentally, the result order of the following function seems _very_ crucial for efficiency. No idea why. Do not remove the List.rev - or modify the current semantics of Util.list_union (some elements of first + or modify the current semantics of Util.List.union (some elements of first arg, then second arg), unless you know what you're doing. *) let rec get_eclatement env = function i :: r -> let l = try (get_equation env i).e_depends with Not_found -> [] in - list_union (List.rev l) (get_eclatement env r) + List.union (List.rev l) (get_eclatement env r) | [] -> [] let select_smaller l = @@ -1031,7 +1031,7 @@ let mk_direction_list l = (* \section{Rejouer l'historique} *) let get_hyp env_hyp i = - try list_index0 (CCEqua i) env_hyp + try List.index0 (CCEqua i) env_hyp with Not_found -> failwith (Printf.sprintf "get_hyp %d" i) let replay_history env env_hyp = @@ -1198,8 +1198,8 @@ let resolution env full_reified_goal systems_list = let useful_equa_id = equas_of_solution_tree solution_tree in (* recupere explicitement ces equations *) let equations = List.map (get_equation env) useful_equa_id in - let l_hyps' = list_uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in - let l_hyps = id_concl :: list_remove id_concl l_hyps' in + let l_hyps' = List.uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in + let l_hyps = id_concl :: List.remove id_concl l_hyps' in let useful_hyps = List.map (fun id -> List.assoc id full_reified_goal) l_hyps in let useful_vars = @@ -1253,7 +1253,7 @@ let resolution env full_reified_goal systems_list = | ((O_left | O_mono) :: l) -> app coq_p_left [| loop l |] | (O_right :: l) -> app coq_p_right [| loop l |] in let correct_index = - let i = list_index0 e.e_origin.o_hyp l_hyps in + let i = List.index0 e.e_origin.o_hyp l_hyps in (* PL: it seems that additionnally introduced hyps are in the way during normalization, hence this index shifting... *) if i=0 then 0 else Pervasives.(+) i (List.length to_introduce) diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index f540349ed8..f838b56c6e 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -87,7 +87,7 @@ let interp_map l c = with Not_found -> None let interp_map l t = - try Some(list_assoc_f eq_constr t l) with Not_found -> None + try Some(List.assoc_f eq_constr t l) with Not_found -> None let protect_maps = ref Stringmap.empty let add_map s m = protect_maps := Stringmap.add s m !protect_maps @@ -194,7 +194,7 @@ let dummy_goal env = Evd.sigma = sigma} let exec_tactic env n f args = - let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in + let lid = List.tabulate(fun i -> id_of_string("x"^string_of_int i)) n in let res = ref [||] in let get_res ist = let l = List.map (fun id -> List.assoc id ist.lfun) lid in @@ -834,7 +834,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl = TACTIC EXTEND ring_lookup | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> - [ let (t,lr) = list_sep_last lrt in ring_lookup f lH lr t] + [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t] END @@ -1162,5 +1162,5 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl = TACTIC EXTEND field_lookup | [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> - [ let (t,l) = list_sep_last lt in field_lookup f lH l t ] + [ let (t,l) = List.sep_last lt in field_lookup f lH l t ] END |