Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name

1 files changed, 9 insertions, 9 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 51eed2f4e..2a1e2b682 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) =
@@ -1671,7 +1671,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 =
         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
@@ -1803,7 +1803,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)))