diff options
| -rw-r--r-- | interp/notation_ops.ml | 8 | ||||
| -rw-r--r-- | kernel/pre_env.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 14 | ||||
| -rw-r--r-- | pretyping/cases.ml | 4 | ||||
| -rw-r--r-- | vernac/command.ml | 2 |
5 files changed, 15 insertions, 15 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 5d703011d..a5ba9bb00 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -104,7 +104,7 @@ let rec cases_pattern_fold_map ?loc g e = CAst.with_val (function let e',na' = g e na in e', CAst.make ?loc @@ PatVar 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_left_map (cases_pattern_fold_map ?loc g) e patl in e', CAst.make ?loc @@ PatCstr (cstr,patl',na') ) @@ -169,18 +169,18 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = 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_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in Loc.tag (idl,patl,f e rhs)) eqnl in GCases (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_left_map g e nal in let e'',na = g e na in GLetTuple (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 (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_left_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 diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 7b4fb4e86..94738d618 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -156,7 +156,7 @@ let map_named_val f ctxt = in (accu, d') in - let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in + let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in if map == ctxt.env_named_map then ctxt else { env_named_ctx = ctx; env_named_map = map } diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index d3e625e73..5f4f5a620 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -689,7 +689,7 @@ let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = (* dest_fun, List.assoc may raise Not_found *) let sigma, c = interp_fun ist env sigma x in sigma, [c] in - let sigma, l = List.fold_map try_expand_ltac_var sigma l in + let sigma, l = List.fold_left_map try_expand_ltac_var sigma l in sigma, List.flatten l let interp_constr_list ist env sigma c = @@ -908,18 +908,18 @@ and interp_intro_pattern_action ist env sigma = function and interp_or_and_intro_pattern ist env sigma = function | IntroAndPattern l -> - let sigma, l = List.fold_map (interp_intro_pattern ist env) sigma l in + let sigma, l = List.fold_left_map (interp_intro_pattern ist env) sigma l in sigma, IntroAndPattern l | IntroOrPattern ll -> - let sigma, ll = List.fold_map (interp_intro_pattern_list_as_list ist env) sigma ll in + let sigma, ll = List.fold_left_map (interp_intro_pattern_list_as_list ist env) sigma ll in sigma, IntroOrPattern ll and interp_intro_pattern_list_as_list ist env sigma = function | [loc,IntroNaming (IntroIdentifier id)] as l -> (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> - List.fold_map (interp_intro_pattern ist env) sigma l) - | l -> List.fold_map (interp_intro_pattern ist env) sigma l + List.fold_left_map (interp_intro_pattern ist env) sigma l) + | l -> List.fold_left_map (interp_intro_pattern ist env) sigma l let interp_intro_pattern_naming_option ist env sigma = function | None -> None @@ -973,7 +973,7 @@ let interp_bindings ist env sigma = function let sigma, l = interp_open_constr_list ist env sigma l in sigma, ImplicitBindings l | ExplicitBindings l -> - let sigma, l = List.fold_map (interp_binding ist env) sigma l in + let sigma, l = List.fold_left_map (interp_binding ist env) sigma l in sigma, ExplicitBindings l let interp_constr_with_bindings ist env sigma (c,bl) = @@ -1775,7 +1775,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = project gl in let sigma,l = - List.fold_map begin fun sigma (c,(ipato,ipats),cls) -> + List.fold_left_map begin fun sigma (c,(ipato,ipats),cls) -> (* TODO: move sigma as a side-effect *) (* spiwack: the [*p] variants are for printing *) let cp = c in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 49f073d66..fe5b90e04 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1753,14 +1753,14 @@ let build_inversion_problem loc env sigma tms t = let cstr,u = destConstruct sigma f in let n = constructor_nrealargs_env 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,acc = List.fold_right_map reveal_pattern l acc in CAst.make (PatCstr (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_right_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 sigma true indf' in diff --git a/vernac/command.ml b/vernac/command.ml index e04bebe33..b831b08f5 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -241,7 +241,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = else l in (* We intepret all declarations in the same evar_map, i.e. as a telescope. *) - let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) -> + let _,l = List.fold_left_map (fun (env,ienv) (is_coe,(idl,c)) -> let t,imps = interp_assumption evdref env ienv [] c in let env = push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in |