diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 2 | ||||
| -rw-r--r-- | proofs/proofview.ml | 8 | ||||
| -rw-r--r-- | proofs/proofview.mli | 17 |
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 *) |