diff options
| -rw-r--r-- | proofs/proofview.ml | 6 | ||||
| -rw-r--r-- | proofs/proofview.mli | 3 |
2 files changed, 9 insertions, 0 deletions
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]. *) |