From 3c992f8540afd7f76eb90a29301e143c465bf280 Mon Sep 17 00:00:00 2001
From: bertot
Date: Fri, 9 Feb 2001 08:18:03 +0000
Subject: exported several functions that are used in the graphical interface
 pcoq.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1363 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.mli | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 3ae29f09af..801eb83eb4 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -22,3 +22,12 @@ 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
+
+(* This function is used to transform a qualified identifier into a
+   global reference, with a nice error message in case of failure.
+   It is used in pcoq. *)
+val global : Coqast.loc -> qualid -> global_reference;;
+
+(* this function is used to analyse the extra arguments in search commands.
+   It is used in pcoq. *)
+val inside_outside : vernac_arg list -> dir_path list * bool;;
-- 
cgit v1.2.3