From e656dd8f414196cec53532b247642de7daeca75b Mon Sep 17 00:00:00 2001
From: bertot
Date: Thu, 8 Feb 2001 07:43:25 +0000
Subject: 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
---
 toplevel/vernacentries.mli | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 68b78ee6ab..3ae29f09af 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
-- 
cgit v1.2.3