diff options
| author | Pierre Courtieu | 2015-01-08 16:59:47 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2015-01-08 16:59:57 +0100 |
| commit | b92fff621cce1576c93fab9276fb41ea85e10982 (patch) | |
| tree | d6e0c1964b274c9b00339452d77468f48ebe2794 /proofs/proofview.mli | |
| parent | 448bf4529c5766e98367345076d00e64e25db7bf (diff) | |
Fixed and extend bullet related info/error messages. + doc.
Had to put some hook in the handler of Proofview.NoSuchgoals.
Documentation updated. CHANGE updated.
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 25f4547a91..adcdeb819e 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -229,8 +229,14 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic (** [tclFOCUS i j t] applies [t] after focusing on the goals number [i] to [j] (see {!focus}). The rest of the goals is restored after the tactic action. If the specified range doesn't correspond to - existing goals, fails with [NoSuchGoals] (a user error). *) + existing goals, fails with [NoSuchGoals] (a user error). this + exception is catched at toplevel with a default message + a hook + message that can be customized by [set_nosuchgoals_hook] below. + This hook is used to add a suggestion about bullets when + applicable. *) exception NoSuchGoals of int +val set_nosuchgoals_hook: (int -> string option) -> unit + val tclFOCUS : int -> int -> 'a tactic -> 'a tactic (** [tclFOCUSID x t] applies [t] on a (single) focused goal like |