Exporting Proof.split in proofview.

2 files changed, 19 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index c478bd6635..0f118a7c6d 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -210,6 +210,10 @@ let unfocus c sp =
 module Proof = Proofview_monad.Logical
 type +'a tactic = 'a Proof.t
 
+type 'a case =
+| Fail of exn
+| Next of 'a * (exn -> 'a tactic)
+
 (* Applies a tactic to the current proofview. *)
 let apply env t sp =
   let (((next_r,next_state),status)) = Proofview_monad.NonLogical.run (Proof.run t env sp) in
@@ -247,6 +251,14 @@ let tclOR t1 t2 =
 (* [tclZERO e] always fails with error message [e]*)
 let tclZERO = Proof.zero
 
+(* [tclCASE t] observes the head of the tactic and returns it as a value *)
+let tclCASE t =
+  let map = function
+  | Nil e -> Fail e
+  | Cons (x, t) -> Next (x, t)
+  in
+  Proof.map map (Proof.split t)
+
 (* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once
    or [t2] if [t1] fails. *)
 let tclORELSE t1 t2 =
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 6a2d815114..affe276800 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -124,6 +124,10 @@ val unfocus : focus_context -> proofview -> proofview
 
 type +'a tactic 
 
+type 'a case =
+| Fail of exn
+| Next of 'a * (exn -> 'a tactic)
+
 (* Applies a tactic to the current proofview. *)
 (* the return boolean signals the use of an unsafe tactic, in which
    case it is [false]. *)
@@ -160,6 +164,9 @@ val tclZERO : exn -> 'a tactic
    or [t2 e] if [t1] fails with [e]. *)
 val tclORELSE : 'a tactic -> (exn -> 'a tactic) -> 'a tactic
 
+(* [tclCASE t] observes the head of the tactic and returns it as a value *)
+val tclCASE : 'a tactic -> 'a case tactic
+
 (* [tclIFCATCH a s f] is a generalisation of [tclORELSE]: if [a]
    succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a]
    fails with [e], then it behaves as [f e]. *)