diff options
Diffstat (limited to 'toplevel/vernacentries.mli')
| -rw-r--r-- | toplevel/vernacentries.mli | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 44e8b7ab46..58df8a9065 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -55,3 +55,14 @@ val abort_refine : ('a -> unit) -> 'a -> unit;; val interp : Vernacexpr.vernac_expr -> unit val vernac_reset_name : identifier Util.located -> unit + +(* Print subgoals when the verbose flag is on. Meant to be used inside + vernac commands from plugins. *) +val print_subgoals : unit -> unit + + +(* Handles focusing/defocusing with bullets: + - If this bullet follows another one of its kind, defocuses then focuses + (which fails if the focused subproof is not complete). + - If it is the first bullet of its kind, then focuses a new subproof. *) +val put_bullet : Proof.proof -> bullet -> unit |