Severe reorganisation of the code of tactics in Proofview.

All the purely monadic code has been moved to a new module Monads,
where, I'm afraid to confess, I got to use a number of proof transformers
to modularise the definition of tactics. It is still not easy to understand (why
would it with backtracking support?) but at least it's more robust, cleaner,
and more extensible. Plus there is now a Proofview.tclORELSE which will
be used to interprete the Ltac tactical (t1 || t2).

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

1 files changed, 7 insertions, 6 deletions

diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index d9cc43e50..ade8be1a3 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -134,13 +134,18 @@ val tclTHEN : unit tactic -> 'a tactic -> 'a tactic
    but drops the value at the end. *)
 val tclIGNORE : 'a tactic -> unit tactic
 
-(* [tclOR t1 t2 = t1] if t1 succeeds and [tclOR t1 t2 = t2] if t2 fails. 
-    No interleaving at this point. *)
+(* [tclOR t1 t2 = t1] as long as [t1] succeeds. Whenever the successes
+   of [t1] have been depleted, then it behaves as [t2].  No
+   interleaving at this point. *)
 val tclOR : 'a tactic -> 'a tactic -> 'a tactic
 
 (* [tclZERO] always fails *)
 val tclZERO : exn -> 'a tactic
 
+(* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once
+   or [t2] if [t1] fails. *)
+val tclORELSE : 'a tactic -> 'a tactic -> 'a tactic
+
 (* Focuses a tactic at a range of subgoals, found by their indices. *)
 val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
 
@@ -229,8 +234,4 @@ module V82 : sig
     
   (* Implements the Existential command *)
   val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview
-
-  (* spiwack: [purify] might be useful while writing tactics manipulating exception 
-     explicitely or from the [V82] submodule (neither being advised, though *)
-  val purify : 'a tactic -> 'a tactic
 end