From 0c133afc50ccfda19c4952abf579b6d94ab5f229 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 18 Aug 2017 01:04:32 +0200 Subject: Adapting code to renaming Option.fold_map -> Option.fold_left_map. --- plugins/ltac/tacinterp.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/ltac/tacinterp.ml') diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 5f4f5a620..6e86b1940 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1657,7 +1657,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = project gl in let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in - let sigma, cbo = Option.fold_map (interp_open_constr_with_bindings ist env) sigma cbo in + let sigma, cbo = Option.fold_left_map (interp_open_constr_with_bindings ist env) sigma cbo in let named_tac = let tac = Tactics.elim ev keep cb cbo in name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac @@ -1789,7 +1789,7 @@ and interp_atomic ist tac : unit Proofview.tactic = in let l,lp = List.split l in let sigma,el = - Option.fold_map (interp_open_constr_with_bindings ist env) sigma el in + Option.fold_left_map (interp_open_constr_with_bindings ist env) sigma el in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (name_atomic ~env (TacInductionDestruct(isrec,ev,(lp,el))) -- cgit v1.2.3