diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2015-06-29 14:11:06 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-14 06:21:30 +0200 |
| commit | 1e19f163b8c7a21d63165784828f4d733aa95171 (patch) | |
| tree | 43e543943c7e1e0465064c39e6331f5b4bcf16a0 /engine | |
| parent | 591b3c37c980a092f0d2abadd8bdf23de3a38bcb (diff) | |
Fix a typo in proofs/proofview.mli.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/proofview.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index 2f8394e84..eecfcdefb 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -240,7 +240,7 @@ 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)] denothing + 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 |