From 1a1af4f2119715245b8d4488664a8b57f4bdce08 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 4 Sep 2016 08:33:51 +0200
Subject: Adding variants enter_one and refine_one which assume that exactly
 one goal is under focus and which support returning a relevant output.

---
 engine/proofview.ml  | 20 ++++++++++++++++++++
 engine/proofview.mli |  4 ++++
 2 files changed, 24 insertions(+)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 576569cf5f..a2838a2de1 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1058,6 +1058,26 @@ module Goal = struct
     end
     end
 
+  exception NotExactlyOneSubgoal
+  let _ = CErrors.register_handler begin function
+  | NotExactlyOneSubgoal ->
+      CErrors.errorlabstrm "" (Pp.str"Not exactly one subgoal.")
+  | _ -> raise CErrors.Unhandled
+  end
+
+  let enter_one f =
+    let open Proof in
+    Comb.get >>= function
+    | [goal] -> begin
+       Env.get >>= fun env ->
+       tclEVARMAP >>= fun sigma ->
+       try f.enter (gmake env sigma goal)
+       with e when catchable_exception e ->
+         let (e, info) = CErrors.push e in
+         tclZERO ~info e
+      end
+    | _ -> tclZERO NotExactlyOneSubgoal
+
   type ('a, 'b) s_enter =
     { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 901cf26e0e..bc68f11ff0 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -499,6 +499,10 @@ module Goal : sig
   (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
   val enter : ([ `LZ ], unit tactic) enter -> unit tactic
 
+  (** Like {!enter}, but assumes exactly one goal under focus, raising *)
+  (** an error otherwise. *)
+  val enter_one : ([ `LZ ], 'a tactic) enter -> 'a tactic
+
   type ('a, 'b) s_enter =
     { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
 
-- 
cgit v1.2.3