diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-08 07:43:25 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-08 07:43:25 +0000 |
| commit | e656dd8f414196cec53532b247642de7daeca75b (patch) | |
| tree | 9cb96cca8d9b3b5978cf7efadc5ffcd068100f36 /toplevel | |
| parent | bc6787e51fdb3b2bb449d288791e963dd7416737 (diff) | |
export a function that can be used to retrieve the context corresponding
to the current goal. This is needed for pcoq.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1352 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |