From 47c688165c6ad00b725bc4f93574bba55c2544f5 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 30 Jul 2014 12:04:18 +0200
Subject: Add primtive [num_goal] to Proofview.

The [num_goal] tactic counts the number of focused goals.
---
 proofs/proofview.ml  | 6 ++++++
 proofs/proofview.mli | 3 +++
 2 files changed, 9 insertions(+)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index aba7691cd4..08a736278e 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -692,6 +692,12 @@ let swap i j =
   in
   Proof.set {initial with comb}
 
+let numgoals =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  Proof.get >>= fun { comb } ->
+  Proof.ret (List.length comb)
+
 (*** Commands ***)
 
 let in_proofview p k =
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index b15d922dcb..b60673ac96 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -282,6 +282,9 @@ val cycle : int -> unit tactic
     [1] as well, rather than raising an error. *)
 val swap : int -> int -> unit tactic
 
+(** [numgoals] returns the number of goals under focus. *)
+val numgoals : int tactic
+
 exception Timeout
 (** [tclTIMEOUT n t] can have only one success.
     In case of timeout if fails with [tclZERO Timeout]. *)
-- 
cgit v1.2.3