diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-18 01:04:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-29 05:11:01 +0200 |
| commit | 0c133afc50ccfda19c4952abf579b6d94ab5f229 (patch) | |
| tree | 44b52aed6249885748aab7317aad9a3873efcc67 /plugins/ltac/tacinterp.ml | |
| parent | 778374f081163b4658b8a2efa72cb332179b3a7d (diff) | |
Adapting code to renaming Option.fold_map -> Option.fold_left_map.
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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))) |