From eb7753109a849aaa7fe5c341f02e408c5fc49f85 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Jul 2014 17:08:59 +0200
Subject: Exporting Proof.split in proofview.

---
 proofs/proofview.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'proofs/proofview.ml')

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 =
-- 
cgit v1.2.3