Code refactoring thanks to the new Monad module.

5 files changed, 7 insertions, 54 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 4d1aa4124..07bdbda00 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -450,31 +450,6 @@ let rename_hyp id1 id2 = (); fun env rdefs gl info ->
   rdefs := Evd.define gl.content new_subproof !rdefs;
   { subgoals = [new_goal] }
 
-(*** Additional functions ***)
-
-(* emulates List.map for functions of type
-   [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating
-   new evar_map to next definition. *)
-(*This sort of construction actually works with any monad (here the State monade
-   in Haskell). There is a generic construction in Haskell called mapM.
-*)
-let rec list_map f l s =
-  match l with
-  | [] -> ([],s)
-  | a::l -> let (a,s) = f s a in
-               let (l,s) = list_map f l s in
-	       (a::l,s)
-
-(* Another instance of the generic monadic map *)
-let rec sensitive_list_map f = function
-  | [] -> return []
-  | a::l ->
-      bind (f a) begin fun a' ->
-      bind (sensitive_list_map f l) begin fun l' ->
-      return (a'::l')
-      end
-      end
-
 
 (* Layer to implement v8.2 tactic engine ontop of the new architecture.
    Types are different from what they used to be due to a change of the
diff --git a/proofs/goal.mli b/proofs/goal.mli
index db864b273..87793878c 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -157,19 +157,6 @@ val defs : Evd.evar_map sensitive
    primitive. *)
 val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> goal -> 'a) -> 'a sensitive
 
-(*** Additional functions ***)
-
-(* emulates List.map for functions of type 
-   [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating
-   new evar_map to next definition *)
-val list_map : 
-  (Evd.evar_map -> 'a -> 'b * Evd.evar_map) ->
-  'a list -> Evd.evar_map ->
-    'b list * Evd.evar_map
-
-(* emulates List.map for [sensitive] Kleisli functions. *)
-val sensitive_list_map : ('a -> 'b sensitive) -> 'a list -> 'b list sensitive
-
 (* Layer to implement v8.2 tactic engine ontop of the new architecture. 
    Types are different from what they used to be due to a change of the
    internal types. *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 0b9aa9907..68be51d9c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -583,7 +583,7 @@ let prim_refiner r sigma goal =
 		  ("Name "^Id.to_string f^" already used in the environment");
 	      mk_sign (push_named_context_val (f,None,ar) sign) oth
 	  | [] ->
-	      Goal.list_map (fun sigma (_,_,c) ->
+	      Evd.Monad.List.map (fun (_,_,c) sigma ->
                 let gl,ev,sig' =
                   Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
                 (gl,ev),sig')
@@ -625,7 +625,7 @@ let prim_refiner r sigma goal =
               |	Not_found ->
                   mk_sign (push_named_context_val (f,None,ar) sign) oth)
 	  | [] -> 
-              Goal.list_map (fun sigma(_,c) ->
+              Evd.Monad.List.map (fun (_,c) sigma ->
                 let gl,ev,sigma =
                   Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
                 (gl,ev),sigma)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 338a8eede..76af0c1e0 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -651,13 +651,6 @@ open Notations
 module Monad =
   Monad.Make(struct type +'a t = 'a tactic let return=tclUNIT let (>>=)=(>>=) end)
 
-let rec list_map f = function
-  | [] -> tclUNIT []
-  | a::l ->
-      f a >>= fun a' ->
-      list_map f l >>= fun l' ->
-      tclUNIT (a'::l')
-
 
 (*** Compatibility layer with <= 8.2 tactics ***)
 module V82 = struct
@@ -670,7 +663,7 @@ module V82 = struct
     let (>>=) = Proof.bind in
     Proof.get >>= fun ps ->
     try
-      let tac evd gl = 
+      let tac gl evd = 
         let glsigma  =
           tac { Evd.it = gl ; sigma = evd; }  in
         let sigma = glsigma.Evd.sigma in
@@ -679,9 +672,9 @@ module V82 = struct
       in
         (* Old style tactics expect the goals normalized with respect to evars. *)
       let (initgoals,initevd) =
-        Goal.list_map Goal.V82.nf_evar ps.comb ps.solution
+        Evd.Monad.List.map (fun g s -> Goal.V82.nf_evar s g) ps.comb ps.solution
       in
-      let (goalss,evd) = Goal.list_map tac initgoals initevd in
+      let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in
       let sgs = List.flatten goalss in
       Proof.set { ps with solution=evd ; comb=sgs; }
     with e when catchable_exception e ->
@@ -696,7 +689,7 @@ module V82 = struct
     let (>>=) = Proof.bind in
     Proof.get >>= fun ps ->
     let (goals,evd) =
-      Goal.list_map Goal.V82.nf_evar ps.comb ps.solution
+      Evd.Monad.List.map (fun g s -> Goal.V82.nf_evar s g) ps.comb ps.solution
     in
     Proof.set { ps with solution=evd ; comb=goals }
 
@@ -796,7 +789,7 @@ module Goal = struct
     Proof.get >>= fun step ->
     try
       let (ks,sigma) =
-        Goal.list_map begin fun sigma g ->
+        Evd.Monad.List.map begin fun g sigma ->
           Util.on_fst k (Goal.eval s env sigma g)
         end step.comb step.solution
       in
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index eba673439..7e2d374d5 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -262,8 +262,6 @@ val mark_as_unsafe : unit tactic
 
 module Monad : Monad.S with type +'a t = 'a tactic
 
-val list_map : ('a -> 'b tactic) -> 'a list -> 'b list tactic
-
 (*** Commands ***)
 
 val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a