diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-30 12:04:18 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-01 19:18:58 +0200 |
| commit | 47c688165c6ad00b725bc4f93574bba55c2544f5 (patch) | |
| tree | 4f74faef9635692fae16fe7b915feed9c3b0519f | |
| parent | f5b2b3ac11763616acc7c418fa566554f2556b4a (diff) | |
Add primtive [num_goal] to Proofview.
The [num_goal] tactic counts the number of focused goals.
| -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 aba7691cd..08a736278 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 b15d922dc..b60673ac9 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]. *) |