From a96aa78636b5fb4ede593b02b1efa2d3025d65d9 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 22 Nov 1999 15:51:26 +0000
Subject: module Tactics (debut)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@129 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml  | 7 +++++++
 library/declare.mli | 2 ++
 2 files changed, 9 insertions(+)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 2220632c66..ff006625a1 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -172,6 +172,13 @@ let global_reference kind id =
   let ids =  ids_of_sign hyps in
   DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
 
+let is_global id =
+  try 
+    let osp = Nametab.sp_of_id CCI id in
+    prefix_of (dirpath osp) (Lib.cwd())
+  with Not_found -> 
+    false
+
 let mind_path = function
   | DOPN(MutInd (sp,0),_) -> sp
   | DOPN(MutInd (sp,tyi),_) -> 
diff --git a/library/declare.mli b/library/declare.mli
index 3a1e7884fb..c2944c330a 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -36,4 +36,6 @@ val declare_mind : mutual_inductive_entry -> unit
 
 val global_reference : path_kind -> identifier -> constr
 
+val is_global : identifier -> bool
+
 val mind_path : constr -> section_path
-- 
cgit v1.2.3