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

4 files changed, 403 insertions, 195 deletions

diff --git a/proofs/monads.ml b/proofs/monads.ml
new file mode 100644
index 000000000..1337931b1
--- /dev/null
+++ b/proofs/monads.ml
@@ -0,0 +1,227 @@
+module type Type = sig
+  type t
+end
+
+module type S = sig
+  type +'a t
+
+  val return : 'a -> 'a t
+  val bind : 'a t -> ('a -> 'b t) -> 'b t
+  val seq : unit t -> 'a t -> 'a t
+  val ignore : 'a t -> unit t
+(* spiwack: these will suffice for now, if we would use monads more
+   globally, then I would add map/join/List.map and such functions,
+   plus default implementations *)
+end
+
+module type State = sig
+  type s (* type of the state *)
+  include S
+
+  val set : s -> unit t
+  val get : s t
+end
+
+module Id : S with type 'a t = 'a = struct
+  type 'a t = 'a
+
+  let return x = x
+  let bind x k = k x
+  let ignore x = Pervasives.ignore x
+  let seq () x = x
+end
+
+(* State monad transformer, adapted from Haskell's StateT *)
+module State (X:Type) (T:S) : sig
+  (* spiwack: it is not essential that both ['a result] and ['a t] be
+     private (or either, for that matter). I just hope it will help
+     catch more programming errors. *)
+  type +'a result = private { result : 'a ; state : X.t }
+  include State with type s = X.t and type +'a t = private X.t -> 'a result T.t
+  (* a function version of the coercion from the private type ['a t].*)
+  val run : 'a t -> s -> 'a result T.t
+  val lift : 'a T.t -> 'a t
+end = struct
+  type s = X.t
+  type 'a result = { result : 'a ; state : s }
+  type 'a t = s -> 'a result T.t
+
+  let run x = x
+  (*spiwack: convenience notation, waiting for ocaml 3.12 *)
+  let (>>=) = T.bind
+  let return x s = T.return { result=x ; state=s }
+  let bind x k s =
+    x s >>= fun { result=a ; state=s } ->
+    k a s
+  let ignore x s =
+    x s >>= fun x' ->
+    T.return { x' with result=() }
+  let seq x t s =
+    (x s) >>= fun x' ->
+    t x'.state
+  let lift x s =
+    x >>= fun a ->
+    T.return { result=a ; state=s }
+
+  let set s _ =
+    T.return { result=() ; state=s }
+  let get s =
+    T.return { result=s ; state=s }
+end
+
+(* Double-continuation backtracking monads are reasonable folklore for
+   "search" implementations (including Tac interactive prover's
+   tactics). Yet it's quite hard to wrap your head around these.  I
+   recommand reading a few times the "Backtracking, Interleaving, and
+   Terminating Monad Transformers" paper by O. Kiselyov, C. Chen,
+   D. Fridman.  The peculiar shape of the monadic type is reminiscent
+   of that of the continuation monad transformer.
+
+   The paper also contains the rational for the [split] abstraction.
+
+   An explanation of how to derive such a monad from mathematical
+   principle can be found in "Kan Extensions for Program Optimisation" by
+   Ralf Hinze. *)
+module type Logic = sig
+  include S
+
+  (* [zero] is usually argument free, but Coq likes to explain errors,
+     hence error messages should be carried around. *)
+  val zero : exn -> 'a t
+  val plus : 'a t -> 'a t -> 'a t
+(** Writing (+) for plus and (>>=) for bind, we shall require that
+
+    zero+x = x
+
+    x+zero = x
+
+    (x+y)>>=k = (x>>=k)+(y>>=k) *)
+
+  (** [split x] runs [x] until it either fails with [zero e] or finds
+      a result [a].  In the former case it returns [Inr e], otherwise
+      it returns [Inl (a,y)] where [y] can be run to get more results
+      from [x]. It is a variant of prolog's cut. *)
+  val split : 'a t -> ('a * 'a t , exn ) Util.union t
+end
+(* The [T] argument represents the "global" effect: it is not
+   backtracked when backtracking occurs at a [plus]. *)
+(* spiwack: hence, [T] will not be instanciated with a state monad
+   representing the proofs, we will use a surrounding state transformer
+   to that effect. In fact at the time I'm writing this comment, I have
+   no immediate use for [T]. We might, however, consider instantiating it
+   with a "writer" monad around [Pp] to implement [idtac "msg"] for
+   instance. *)
+module Logic (T:S) : sig
+  include Logic
+
+  (** [run x] raises [e] if [x] is [zero e]. *)
+  val run : 'a t -> 'a T.t
+
+  val lift : 'a T.t -> 'a t
+end = struct
+(* spiwack: the implementation is an adaptation of the aforementionned
+   "Backtracking, Interleaving, and Terminating Monad Transformers"
+   paper *)
+  (* spiwack: [fk] stands for failure continuation, and [sk] for success
+     continuation. *)
+  type +'r fk = exn -> 'r
+  type (-'a,'r) sk = 'a -> 'r fk -> 'r
+  type 'a t = { go : 'r. ('a,'r T.t) sk -> 'r T.t fk -> 'r T.t }
+
+  let return x = { go = fun sk fk ->
+    sk x fk
+                 }
+  let bind x k = { go = fun sk fk ->
+    x.go (fun a fk -> (k a).go sk fk) fk
+                 }
+  let ignore x = { go = fun sk fk ->
+    x.go (fun _ fk -> sk () fk) fk
+                 }
+  let seq x t = { go = fun sk fk ->
+    x.go (fun () fk -> t.go sk fk) fk
+                }
+
+  let zero e = { go = fun _ fk -> fk e }
+  (* [plus x y] ignores any error raised by [x]. *)
+  let plus x y = { go = fun sk fk ->
+    x.go sk (fun _ -> y.go sk fk)
+                 }
+
+  let lift x = { go = fun sk fk ->
+    T.bind x (fun a -> sk a fk)
+               }
+
+  let run x =
+    let sk a _ = T.return a in
+    let fk e = raise e in
+    x.go sk fk
+
+  (* For [reflect] and [split] see the "Backtracking, Interleaving,
+     and Terminating Monad Transformers" paper *)
+  let reflect : ('a*'a t , exn) Util.union -> 'a t = function
+    | Util.Inr e -> zero e
+    | Util.Inl (a,x) -> plus (return a) x
+
+  let split x =
+    (* spiwack: I cannot be sure right now, but [anomaly] shouldn't be
+       reachable. If it is reachable there may be some redesign to be
+       done around success continuations. *)
+    let anomaly = Errors.Anomaly ("Monads.Logic(T).split", Pp.str"[fk] should ignore this error") in
+    let fk e = T.return (Util.Inr e) in
+    let sk a fk = T.return (Util.Inl (a,bind (lift (fk anomaly)) reflect)) in
+    lift (x.go sk fk)
+end
+
+
+(* [State(X)(T:Logic)] can be lifted to [Logic] by backtracking on state on [plus].*)
+module StateLogic(X:Type)(T:Logic) : sig
+  (* spiwack: some duplication from interfaces as we need ocaml 3.12
+     to substitute inside signatures. *)
+  type s = X.t
+  type +'a result = private { result : 'a ; state : s }
+  include Logic with type +'a t = private X.t -> 'a result T.t
+
+  val set : s -> unit t
+  val get : s t
+
+  val run : 'a t -> s -> 'a result T.t
+end = struct
+
+  module S = State(X)(T)
+  include S
+
+  let zero e = lift (T.zero e)
+  let plus x y =
+    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
+    let (>>=) = bind in
+    let (>>) = seq in
+    get >>= fun initial ->
+    lift begin
+      (T.plus (run x initial) (run y initial)) 
+    end >>= fun { result = a ; state = final } ->
+    set final >>
+    return a
+  (* spiwack: the definition of [plus] is essentially [plus x y = fun s
+     -> T.plus (run x s) (run y s)]. But the [private] annotation
+     prevents us from writing that. Maybe I should remove [private]
+     around [+'a t] (it would be unnecessary to remove that of ['a
+     result]) after all. I'll leave it like that for now. *)
+
+  let split x =
+    (* spiwack: convenience notation, waiting for ocaml 3.12 *)
+    let (>>=) = bind in
+    let (>>) = seq in
+    get >>= fun initial ->
+    lift (T.split (run x initial)) >>= function
+      | Util.Inr _ as e -> return e
+      | Util.Inl (a,y) ->
+          let y' =
+            lift y >>= fun b ->
+            set b.state >>
+            return b.result
+          in
+          set a.state >>
+          return (Util.Inl(a.result,y'))
+end
+
+
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index ca0c7dd0d..96af73b71 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,5 +1,6 @@
 Goal
 Evar_refiner
+Monads
 Proofview
 Proof
 Proof_global
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 00e311cc9..347783a66 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -173,104 +173,78 @@ let unfocus c sp =
      specialized bind on unit-returning tactics).
 *)
 
-(* type of tactics *)
-(* spiwack: double-continuation backtracking monads are reasonable
-    folklore for "search" implementations (including Tac interactive prover's
-    tactics). Yet it's quite hard to wrap your head around these.
-    I recommand reading a few times the "Backtracking, Interleaving, and Terminating
-    Monad Transformers" paper by O. Kiselyov, C. Chen, D. Fridman.  
-    The peculiar shape of the monadic type is reminiscent of that of the continuation
-    monad transformer.
-    A good way to get a feel of what's happening is to look at what happens when
-    executing [apply (tclUNIT ())]. 
-    The disjunction function is unlike that of the LogicT paper, because we want and 
-    need to backtrack over state as well as values. Therefore we cannot be
-    polymorphic over the inner monad. *)
-type proof_step = { goals : Goal.goal list ; defs : Evd.evar_map }
-type +'a result = { proof_step : proof_step ;
-		                content : 'a }
-
-(* nb=non-backtracking *)
-type +'a nb_tactic  = proof_step -> 'a result
-
-(* double-continutation backtracking *)
-(* "sk" stands for "success continuation", "fk" for "failure continuation" *)
-type 'r fk = exn -> 'r
-type (-'a,'r) sk = 'a -> 'r fk -> 'r
-type +'a tactic0 = { go : 'r. ('a, 'r nb_tactic) sk -> 'r nb_tactic fk -> 'r nb_tactic }
-
-(* We obtain a tactic by parametrizing with an environment *)
-(* spiwack: alternatively the environment could be part of the "nb_tactic" state
-    monad. As long as we do not intend to change the environment during a tactic,
-    it's probably better here. *)
-type +'a tactic = Environ.env -> 'a tactic0
-
-(* unit of [nb_tactic] *)
-let nb_tac_unit a step = { proof_step = step ; content = a }
+(* type of tactics:
+
+   tactics can
+   - access the environment,
+   - access and change the current [proofview]
+   - backtrack on previous changes of the proofview *)
+(* spiwack: it seems lighter, for now, to deal with the environment here rather than in [Monads]. *)
+
+module LocalState = struct
+  type t = proofview
+end
+module Backtrack = Monads.Logic(Monads.Id)
+module Inner = Monads.StateLogic(LocalState)(Backtrack)
+
+type +'a tactic = Environ.env -> 'a Inner.t
 
 (* Applies a tactic to the current proofview. *)
-let apply env t sp  = 
-  let start = { goals = sp.comb ; defs = sp.solution } in
-  let res = (t env).go (fun a _ step -> nb_tac_unit a step) (fun e _ -> raise e) start in
-  let next = res.proof_step in
-  {sp with
-     solution = next.defs ;
-     comb = next.goals
-  }
+let apply env t sp =
+  let next = Backtrack.run (Inner.run (t env) sp) in
+  next.Inner.state
 
 (*** tacticals ***)
 
 
 (* Unit of the tactic monad *)
-let tclUNIT a _ = { go = fun sk fk step -> sk a fk step }
+let tclUNIT a _ = Inner.return a
 
 (* Bind operation of the tactic monad *)
-let tclBIND t k env = { go = fun sk fk step ->
-  (t env).go (fun a fk -> (k a env).go sk fk) fk step
-}
+let tclBIND t k env =
+  Inner.bind (t env) (fun a -> k a env)
 
 (* Interpretes the ";" (semicolon) of Ltac.
    As a monadic operation, it's a specialized "bind"
    on unit-returning tactic (meaning "there is no value to bind") *)
-let tclTHEN t1 t2 env = { go = fun sk fk step ->
-  (t1 env).go (fun () fk -> (t2 env).go sk fk) fk step
-}
+let tclTHEN t1 t2 env =
+  Inner.seq (t1 env) (t2 env)
 
 (* [tclIGNORE t] has the same operational content as [t],
    but drops the value at the end. *)
-let tclIGNORE tac env = { go = fun sk fk step ->
-  (tac env).go (fun _ fk -> sk () fk) fk step
-}
-
-(* [tclOR t1 t2 = t1] if t1 succeeds and [tclOR t1 t2 = t2] if t1 fails. 
-    No interleaving for the moment. *)
-(* spiwack: compared to the LogicT paper, we backtrack at the same state
-    where [t1] has been called, not the state where [t1] failed. *)
-let tclOR t1 t2 env = { go = fun sk fk step ->
-  (t1 env).go sk (fun _ _ -> (t2 env).go sk fk step) step
-}
-
-(* [tclZERO e] always fails with error message [e]*)
-let tclZERO e env = { go = fun _ fk step -> fk e step }
+let tclIGNORE tac env = Inner.ignore (tac env)
 
+(* [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. *)
+let tclOR t1 t2 env =
+  Inner.plus (t1 env) (t2 env)
 
-(* Focusing operation on proof_steps. *)
-let focus_proof_step i j ps =
-  let (new_subgoals, context) = focus_sublist i j ps.goals in
-  ( { ps with goals = new_subgoals } , context )
+(* [tclZERO e] always fails with error message [e]*)
+let tclZERO e _ = Inner.zero e
 
-(* Unfocusing operation of proof_steps. *)
-let unfocus_proof_step c ps =
-  { ps with 
-     goals = undefined ps.defs (unfocus_sublist c ps.goals) 
-  }
+(* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once
+   or [t2] if [t1] fails. *)
+let tclORELSE t1 t2 env =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Inner.bind in
+  Inner.split (t1 env) >>= function
+    | Util.Inr _ -> t2 env
+    | Util.Inl (a,t1') -> Inner.plus (Inner.return a) t1'
 
 (* Focuses a tactic at a range of subgoals, found by their indices. *)
 (* arnaud: bug if 0 goals ! *)
-let tclFOCUS i j t env = { go = fun sk fk step ->
-  let (focused,context) = focus_proof_step i j step in
-  (t env).go (fun a fk step -> sk a fk (unfocus_proof_step context step)) fk focused
-}
+let tclFOCUS i j t env =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Inner.bind in
+  let (>>) = Inner.seq in
+  Inner.get >>= fun initial ->
+  let (focused,context) = focus i j initial in
+  Inner.set focused >>
+  t (env) >>= fun result ->
+  Inner.get >>= fun next ->
+  Inner.set (unfocus context next) >>
+  Inner.return result
 
 (* Dispatch tacticals are used to apply a different tactic to each goal under
     consideration. They come in two flavours:
@@ -292,111 +266,67 @@ end
     the return value at two given lists of subgoals are combined when
     both lists are being concatenated.
     [join] and [null] need be some sort of comutative monoid. *)
-let rec tclDISPATCHGEN null join tacs env = { go = fun sk fk step ->
-  match tacs,step.goals with
-  | [] , [] -> (tclUNIT null env).go sk fk step
-  | t::tacs , first::goals -> 
-      (tclDISPATCHGEN null join tacs env).go
-	begin fun x fk step -> 
-	  match Goal.advance step.defs first with
-	  | None -> sk x fk step
-	  | Some first ->
-	    (t env).go 
-	      begin fun y fk step' -> 
-		sk (join x y) fk { step' with 
-			                   goals = step'.goals@step.goals
-				         }
-	      end 
-	      fk 
-	      { step with goals = [first] }
-	end
-	fk
-	{ step with goals = goals }
-  | _ -> raise SizeMismatch
-}
-
-(* takes a tactic which can raise exception and makes it pure by *failing* 
-    on with these exceptions. Does not catch anomalies. *)
-let purify t = 
-  let t' env = { go = fun sk fk step -> try (t env).go (fun x -> sk (Util.Inl x)) fk step
-     	                                                     with Errors.Anomaly _ as e -> raise e
-							           | e -> sk (Util.Inr e) fk step
-	       }
-  in
-  tclBIND t' begin function
-    | Util.Inl x -> tclUNIT x
-    | Util.Inr e -> tclZERO e
-  end
-let tclDISPATCHGEN null join tacs = purify (tclDISPATCHGEN null join tacs)
+let rec tclDISPATCHGEN null join tacs env =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Inner.bind in
+  let (>>) = Inner.seq in
+  Inner.get >>= fun initial ->
+  match tacs,initial.comb with
+  | [], [] -> tclUNIT null env
+  | t::tacs , first::goals ->
+      Inner.set {initial with comb=goals} >>
+      tclDISPATCHGEN null join tacs env >>= fun x ->
+      Inner.get >>= fun step ->
+      begin match Goal.advance step.solution first with
+      | None -> Inner.return x (* If [first] has been solved by side effect: do nothing. *)
+      | Some first ->
+          Inner.set {step with comb=[first]} >>
+          t env >>= fun y ->
+          Inner.get >>= fun step' ->
+          Inner.set {step' with comb=step'.comb@step.comb} >>
+          Inner.return (join x y)
+      end
+  | _ , _ -> raise SizeMismatch
 
 let unitK () () = ()
 let tclDISPATCH = tclDISPATCHGEN () unitK
 
-let extend_to_list =
-  let rec copy n x l =
-    if n < 0 then raise SizeMismatch
-    else if n = 0 then l
-    else copy (n-1) x (x::l)
-  in
-  fun startxs rx endxs l ->
-    let ns = List.length startxs in
-    let ne = List.length endxs in
-    let n = List.length l in
-    startxs@(copy (n-ne-ns) rx endxs)
-let tclEXTEND tacs1 rtac tacs2 env = { go = fun sk fk step -> 
-  let tacs = extend_to_list tacs1 rtac tacs2 step.goals in
-  (tclDISPATCH tacs env).go sk fk step
-}
-
-(* [tclGOALBIND] and [tclGOALBINDU] are sorts of bind which take a
-    [Goal.sensitive] as a first argument, the tactic then acts on each goal separately.
-    Allows backtracking between goals. *)
-let list_of_sensitive s k env step =
-  Goal.list_map begin fun defs g ->
-    let (a,defs) = Goal.eval s env defs g in
-    (k a) , defs
-  end step.goals step.defs
-(* In form of a tactic *)
-let list_of_sensitive s k env = { go = fun sk fk step ->
-  let (tacs,defs) = list_of_sensitive s k env step in
-  sk tacs fk { step with defs = defs } 
-}
-
 (* This is a helper function for the dispatching tactics (like [tclGOALBIND] and
     [tclDISPATCHS]). It takes an ['a sensitive] value, and returns a tactic
     whose return value is, again, ['a sensitive] but only has value in the
     (unmodified) goals under focus. *)
-let here_s b env = { go = fun sk fk step ->
-  sk (Goal.bind (Goal.here_list step.goals b) (fun b -> b)) fk step
-}
+let here_s b env =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Inner.bind in
+  Inner.get >>= fun step ->
+  Inner.return (Goal.bind (Goal.here_list step.comb b) (fun b -> b))
 
-let rec tclGOALBIND s k = 
-  (* spiwack: the first line ensures that the value returned by the tactic [k] will
-      not "escape its scope". *)
-  let k a = tclBIND (k a) here_s in
-  purify begin 
-    tclBIND (list_of_sensitive s k) begin fun tacs ->
-      tclDISPATCHGEN Goal.null Goal.plus tacs
-    end 
-  end
-
-(* spiwack: this should probably be moved closer to the [tclDISPATCH] tactical. *)
+(* see .mli for documentation. *)
 let tclDISPATCHS tacs = 
   let tacs = 
     List.map begin fun tac -> 
       tclBIND tac here_s
     end tacs 
   in
-  purify begin 
-    tclDISPATCHGEN Goal.null Goal.plus tacs
-  end
+  tclDISPATCHGEN Goal.null Goal.plus tacs
 
-let rec tclGOALBINDU s k = 
-  purify begin 
-    tclBIND (list_of_sensitive s k) begin fun tacs ->
-      tclDISPATCHGEN () unitK tacs
-    end
-  end
+let extend_to_list =
+  let rec copy n x l =
+    if n < 0 then raise SizeMismatch
+    else if n = 0 then l
+    else copy (n-1) x (x::l)
+  in
+  fun startxs rx endxs l ->
+    let ns = List.length startxs in
+    let ne = List.length endxs in
+    let n = List.length l in
+    startxs@(copy (n-ne-ns) rx endxs)
+let tclEXTEND tacs1 rtac tacs2 env =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Inner.bind in
+  Inner.get >>= fun step ->
+  let tacs = extend_to_list tacs1 rtac tacs2 step.comb in
+  tclDISPATCH tacs env
 
 (* spiwack: up to a few details, same errors are in the Logic module.
     this should be maintained synchronized, probably. *)
@@ -416,9 +346,48 @@ let rec catchable_exception = function
       (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
   | _ -> false
 
+
+(* [tclGOALBIND] and [tclGOALBINDU] are sorts of bind which take a
+    [Goal.sensitive] as a first argument, the tactic then acts on each goal separately.
+    Allows backtracking between goals. *)
+
+(* [list_of_sensitive s k] where [s] is and ['a Goal.sensitive] [k]
+   has type ['a -> 'b] returns the list of ['b] obtained by evualating
+   [s] to each goal successively and applying [k] to each result. *)
+let list_of_sensitive s k env step =
+  Goal.list_map begin fun defs g ->
+    let (a,defs) = Goal.eval s env defs g in
+    (k a) , defs
+  end step.comb step.solution
+(* In form of a tactic *)
+let list_of_sensitive s k env =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Inner.bind in
+  let (>>) = Inner.seq in
+  Inner.get >>= fun step ->
+  try 
+    let (tacs,defs) = list_of_sensitive s k env step in
+    Inner.set { step with solution = defs } >>
+    Inner.return tacs
+  with e when catchable_exception e ->
+    tclZERO e env
+
+let rec tclGOALBIND s k = 
+  (* spiwack: the first line ensures that the value returned by the tactic [k] will
+      not "escape its scope". *)
+  let k a = tclBIND (k a) here_s in
+  tclBIND (list_of_sensitive s k) begin fun tacs ->
+    tclDISPATCHGEN Goal.null Goal.plus tacs
+  end
+
+let rec tclGOALBINDU s k = 
+  tclBIND (list_of_sensitive s k) begin fun tacs ->
+    tclDISPATCHGEN () unitK tacs
+  end
+
 (* No backtracking can happen here, hence, as opposed to the dispatch tacticals,
     everything is done in one step. *)
-let sensitive_on_step s env step =
+let sensitive_on_proofview s env step =
   let wrap g ((defs, partial_list) as partial_res) = 
     match Goal.advance defs g with
     | None ->partial_res
@@ -427,14 +396,20 @@ let sensitive_on_step s env step =
       (d',sg::partial_list)
   in
   let ( new_defs , combed_subgoals ) = 
-    List.fold_right wrap step.goals (step.defs,[])
+    List.fold_right wrap step.comb (step.solution,[])
   in
-  { defs = new_defs;
-     goals = List.flatten combed_subgoals }
-let tclSENSITIVE s =
-  purify begin
-    fun env -> { go = fun sk fk step -> sk () fk (sensitive_on_step s env step) }
-  end
+  { step with
+     solution = new_defs;
+     comb = List.flatten combed_subgoals }
+let tclSENSITIVE s env =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Inner.bind in
+  Inner.get >>= fun step ->
+  try
+    let next = sensitive_on_proofview s env step in
+    Inner.set next
+  with e when catchable_exception e ->
+    tclZERO e env
 
 
 (*** Commands ***)
@@ -457,23 +432,28 @@ end
 module V82 = struct
   type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
-  let tactic tac _ = { go = fun sk fk ps ->
+  let tactic tac env =
     (* spiwack: we ignore the dependencies between goals here, expectingly
-         preserving the semantics of <= 8.2 tactics *)
-    let tac evd gl = 
-      let glsigma  = tac { Evd.it = gl ; Evd.sigma = evd }  in
-      let sigma = glsigma.Evd.sigma in
-      let g = glsigma.Evd.it in
-      ( g , sigma )
-    in
+       preserving the semantics of <= 8.2 tactics *)
+    (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+    let (>>=) = Inner.bind in
+    Inner.get >>= fun ps ->
+    try
+      let tac evd gl = 
+        let glsigma  = tac { Evd.it = gl ; Evd.sigma = evd }  in
+        let sigma = glsigma.Evd.sigma in
+        let g = glsigma.Evd.it in
+        ( g , sigma )
+      in
     (* Old style tactics expect the goals normalized with respect to evars. *)
-    let (initgoals,initevd) = 
-      Goal.list_map Goal.V82.nf_evar ps.goals ps.defs
-    in
-    let (goalss,evd) = Goal.list_map tac initgoals initevd in
-    let sgs = List.flatten goalss in
-    sk () fk { defs = evd ; goals = sgs }
-}
+      let (initgoals,initevd) = 
+        Goal.list_map Goal.V82.nf_evar ps.comb ps.solution
+      in
+      let (goalss,evd) = Goal.list_map tac initgoals initevd in
+      let sgs = List.flatten goalss in
+      Inner.set { ps with solution=evd ; comb=sgs }
+    with e when catchable_exception e ->
+      tclZERO e env
 
   let has_unresolved_evar pv =
     Evd.has_undefined pv.solution
@@ -517,5 +497,4 @@ module V82 = struct
     { pv with
 	solution = Evar_refiner.instantiate_pf_com evk com pv.solution }
 
-  let purify = purify
 end
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