Get rid of the enterl/glist API for Proofview.Goal.

The prefered style is to use continuation passing style when necessary, or simply passing the goal explicitely in the case of interpretation functions which do not evolve the current goal.

5 files changed, 19 insertions, 61 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 49615a5f88..d42ea8b804 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -639,22 +639,9 @@ let in_proofview p k =
   k p.solution
 
 
-(* spiwack: to help using `bind' like construct consistently. A glist
-   is promissed to have exactly one element per goal when it is
-   produced. *)
-type 'a glist  = 'a list
 
 module Notations = struct
   let (>=) = tclBIND
-  let (>>=) t k =
-    t >= fun l ->
-    tclDISPATCHGEN k ignore l
-  let (>>==) t k =
-    begin
-      t >= fun l ->
-      tclDISPATCHGEN k List.rev l
-    end >= fun l' ->
-    tclUNIT (List.flatten l')
   let (<*>) = tclTHEN
   let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
 end
@@ -797,26 +784,24 @@ module Goal = struct
   let hyps { hyps=hyps } = Environ.named_context_of_val hyps
   let concl { concl=concl } = concl
 
-  let lift s =
+  let lift s k =
     (* spiwack: convenience notations, waiting for ocaml 3.12 *)
     let (>>=) = Proof.bind in
     let (>>) = Proof.seq in
     Proof.current >>= fun env ->
     Proof.get >>= fun step ->
     try
-      let (res,sigma) =
+      let (ks,sigma) =
         Goal.list_map begin fun sigma g ->
-          Goal.eval s env sigma g
+          Util.on_fst k (Goal.eval s env sigma g)
         end step.comb step.solution
       in
       Proof.set { step with solution=sigma } >>
-        Proof.ret res
+      tclDISPATCH ks
     with e when catchable_exception e ->
       let e = Errors.push e in
       tclZERO e
 
-  let return x = lift (Goal.return x)
-
   let enter_t f = Goal.enter begin fun env sigma hyps concl self ->
     f {env=env;sigma=sigma;hyps=hyps;concl=concl;self=self}
   end
@@ -832,20 +817,6 @@ module Goal = struct
         let e = Errors.push e in
         tclZERO e
     end
-  let enterl f =
-    list_iter_goal [] begin fun goal acc ->
-      Proof.current >= fun env ->
-      tclEVARMAP >= fun sigma ->
-      try
-        (* enter_t cannot modify the sigma. *)
-        let (t,_) = Goal.eval (enter_t f) env sigma goal in
-        t >= fun r ->
-        tclUNIT (r::acc)
-      with e when catchable_exception e ->
-        let e = Errors.push e in
-        tclZERO e
-    end >= fun res ->
-    tclUNIT (List.flatten (List.rev res))
 
 
   (* compatibility *)
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 021155c425..c608bc8414 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -266,11 +266,6 @@ val list_map : ('a -> 'b tactic) -> 'a list -> 'b list tactic
 
 val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a
 
-(* spiwack: to help using `bind' like construct consistently. A glist
-   is promissed to have exactly one element per goal when it is
-   produced. *)
-type 'a glist  = private 'a list
-
 (* Notations for building tactics. *)
 module Notations : sig
 
@@ -280,10 +275,6 @@ module Notations : sig
      The [t] is supposed to return a list of values of the size of the
      list of goals. [k] is then applied to each of this value in the
      corresponding goal. *)
-  val (>>=) : 'a glist tactic -> ('a -> unit tactic) -> unit tactic
-  (* [t >>== k] acts as [t] except that [k] returns a list of value
-     corresponding to its produced subgoals. *)
-  val (>>==) : 'a glist tactic -> ('a -> 'b glist tactic) -> 'b glist tactic
 
   (* tclTHEN *)
   val (<*>) : unit tactic -> 'a tactic -> 'a tactic
@@ -356,20 +347,14 @@ module Goal : sig
   val env : t -> Environ.env
   val sigma : t -> Evd.evar_map
 
-  (* [lift_sensitive s] returns the list corresponding to the evaluation
-     of [s] on each of the focused goals *)
-  val lift : 'a Goal.sensitive -> 'a glist tactic
-
-  (* [return x] returns a copy of [x] per focused goal. *)
-  val return : 'a -> 'a glist tactic
+  (* [lift_sensitive s k] applies [s] in each goal independently
+     raising result [a] then continues with [k a]. *)
+  val lift : 'a Goal.sensitive -> ('a->unit tactic) -> unit tactic
 
   (* [enter t] execute the goal-dependent tactic [t] in each goal
      independently. In particular [t] need not backtrack the same way in
      each goal. *)
   val enter : (t -> unit tactic) -> unit tactic
-  (* [enterl t] works like [enter t] except that [t] returns a value
-     in each of the produced subgoals. *)
-  val enterl : (t -> 'a glist tactic) -> 'a glist tactic
 
 
   (* compatibility: avoid if possible *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a1e57fd3c4..033a4dc1b3 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -344,9 +344,10 @@ let refine_tac (ist, c) =
         let tycon = Pretyping.OfType concl in
         Goal.Refinable.constr_of_raw h tycon flags vars c)
     end in
-    Proofview.Goal.lift c >>= fun c ->
-    Proofview.tclSENSITIVE (Goal.refine c) <*>
-    Proofview.V82.tactic (reduce refine_red_flags refine_locs))
+    Proofview.Goal.lift c begin fun c ->
+      Proofview.tclSENSITIVE (Goal.refine c) <*>
+      Proofview.V82.tactic (reduce refine_red_flags refine_locs)
+    end)
 
 TACTIC EXTEND refine
   [ "refine" glob(c) ] -> [  refine_tac c ]
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index a10b62162a..853215a5ab 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1305,7 +1305,7 @@ let cl_rewrite_clause_newtac ?abs strat clause =
 	   | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
 	     raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
 			++ fnl () ++ Himsg.explain_typeclass_error env e)))
-  in Proofview.Notations.(>>=) (Proofview.Goal.lift info) (fun i -> treat i)
+  in Proofview.Goal.lift info (fun i -> treat i)
 
 let newtactic_init_setoid () =
   try init_setoid (); Proofview.tclUNIT ()
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b4fb6b9002..b4b6934f25 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3937,11 +3937,12 @@ module New = struct
     let c = Goal.Refinable.make begin fun h ->
       Goal.Refinable.constr_of_open_constr h true c
     end in
-    Proofview.Goal.lift c >>= fun c ->
-    Proofview.tclSENSITIVE (Goal.refine c) <*>
-    Proofview.V82.tactic (reduce
-       (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]})
-       {onhyps=None; concl_occs=AllOccurrences }
-    )
+    Proofview.Goal.lift c begin fun c ->
+      Proofview.tclSENSITIVE (Goal.refine c) <*>
+      Proofview.V82.tactic (reduce
+         (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]})
+         {onhyps=None; concl_occs=AllOccurrences }
+      )
+    end
 
 end