diff options
Diffstat (limited to 'plugins/decl_mode/decl_mode.mli')
| -rw-r--r-- | plugins/decl_mode/decl_mode.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index 538d8944d..c54dcdc28 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -70,6 +70,8 @@ val get_stack : Proof.proof -> stack_info list val get_top_stack : Proof.proof -> stack_info list val get_last: Environ.env -> Id.t +(** [get_last] raises a [UserError] when it cannot find a previous + statement in the environment. *) val focus : Proof.proof -> unit |