diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-16 15:24:56 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-16 16:02:48 +0200 |
| commit | 6aac2c78ad5dec79c6ed16a50accde57c37398a9 (patch) | |
| tree | 53968b5035fd9b70d4431130cf12621f314cb187 /engine/proofview.mli | |
| parent | a452e436af72ccc1b8342ac6b666f0ff202cc20a (diff) | |
| parent | 791f3254cba602672b834ec3484d308db074b684 (diff) | |
Merge 'pr/191' into trunk
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index 93ba55c61..bbf2d6bf7 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -239,6 +239,16 @@ val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit val tclFOCUS : int -> int -> 'a tactic -> 'a tactic +(** [tclFOCUSLIST li t] applies [t] on the list of focused goals + described by [li]. Each element of [li] is a pair [(i, j)] denoting + the goals numbered from [i] to [j] (inclusive, starting from 1). + It will try to apply [t] to all the valid goals in any of these + intervals. If the set of such goals is not a single range, then it + will move goals such that it is a single range. (So, for + instance, [[1, 3-5]; idtac.] is not the identity.) + If the set of such goals is empty, it will fail. *) +val tclFOCUSLIST : (int * int) list -> 'a tactic -> 'a tactic + (** [tclFOCUSID x t] applies [t] on a (single) focused goal like {!tclFOCUS}. The goal is found by its name rather than its number.*) |