diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 68b78ee6a..3ae29f09a 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -19,3 +19,6 @@ val show_nth_open_subgoal : int -> unit val show_open_subgoals_focused : unit -> unit val show_node : unit -> unit +(* This function can be used by any command that want to observe terms + in the context of the current goal, as for instance in pcoq *) +val get_current_context_of_args : vernac_arg list -> Proof_type.enamed_declarations * Environ.env |