Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16971 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 10 insertions, 17 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 76cf41c50..7874f5ac6 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -85,7 +85,7 @@ let elim_res_pf_THEN_i clenv tac gls =
 
 open Proofview.Notations
 let new_elim_res_pf_THEN_i clenv tac =
-  Tacmach.New.of_old (clenv_unique_resolver ~flags:elim_flags clenv) >>- fun clenv' ->
+  Tacmach.New.of_old (clenv_unique_resolver ~flags:elim_flags clenv) >>= fun clenv' ->
   Proofview.tclTHEN
     (Proofview.V82.tactic (clenv_refine false clenv'))
     (Proofview.tclEXTEND [] (Proofview.tclUNIT()) (Array.to_list (tac clenv')))
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index bac4c22cd..406de8d2b 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -168,7 +168,7 @@ let unfocus c sp =
      meta-level as OCaml functions.
      Most tactics, in the sense we are used to, return [ () ], that is
      no really interesting values. But some might pass information 
-     around; the [(>>--)] and [(>>==)] bind-like construction are the
+     around; the [(>>==)] and [(>>==)] bind-like construction are the
      main ingredients of this information passing. 
      (* spiwack: I don't know how much all this relates to F. Kirchner and 
         C. Muñoz. I wasn't able to understand how they used the monad
@@ -409,7 +409,7 @@ type 'a glist  = 'a list
 module Notations = struct
   let (>-) = Goal.bind
   let (>=) = tclBIND
-  let (>>-) t k =
+  let (>>=) t k =
     (* spiwack: the application of List.map may raise errors, as this
        combinator is mostly used in porting historical tactic code,
        where the error flow is somewhat hard to follow, hence the
@@ -417,7 +417,7 @@ module Notations = struct
       t >= fun l ->
       try tclDISPATCH (List.map k l)
       with e when Errors.noncritical e -> tclZERO e
-  let (>>--) t k =
+  let (>>==) t k =
     (* spiwack: the application of List.map may raise errors, as this
        combinator is mostly used in porting historical tactic code,
        where the error flow is somewhat hard to follow, hence the
@@ -428,8 +428,6 @@ module Notations = struct
       with e when Errors.noncritical e -> tclZERO e
     end >= fun l' ->
     tclUNIT (List.flatten l')
-  let (>>=) = (>>-)
-  let (>>==) = (>>--)
   let (<*>) = tclTHEN
   let (<+>) t1 t2 = tclOR t2 (fun _ -> t2)
 end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 261311592..2a69ccaf3 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -212,21 +212,16 @@ type 'a glist  = private 'a list
 module Notations : sig
   (* Goal.bind *)
   val (>-) : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive) -> 'b Goal.sensitive
-  (* [t >>- k] is [tclBIND t (fun l -> tclDISPATCH (List.map k l))] *)
-  val (>>-) : 'a glist tactic -> ('a -> unit tactic) -> unit tactic
-  (* arnaud: commenter *)
-  val (>>--) : 'a glist tactic -> ('a -> 'b glist tactic) -> 'b glist tactic
 
   (* tclBIND *)
   val (>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
-
-  (* arnaud: commentaire à mettre à jour *)
-  (* [(>>=)] (and its goal sensitive variant [(>>==)]) "binds" in one step the
-      tactic monad and the goal-sensitive monad.
-      It is strongly advised to use it everytieme an ['a Goal.sensitive tactic]
-      needs a bind, since it usually avoids to delay the interpretation of the
-      goal sensitive value to a location where it does not make sense anymore. *)
+  (* [t >>= k] is [t >= fun l -> tclDISPATCH (List.map k l)].
+     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 *)