From 2a4ea1915c391ba39b99e4fb17d8354278eec212 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 13 Sep 2003 10:34:26 +0000
Subject: Deplacement de Declare vers Termops

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4396 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/termops.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/termops.mli')

diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 9c9243c8c..9031ec42d 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -180,6 +180,7 @@ val global_vars_set_of_decl : env -> named_declaration -> Idset.t
 
 val construct_reference : named_context -> identifier -> constr
 val global_reference : identifier -> constr
+val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
 (* Test if an identifier is the basename of a global reference *)
 val is_global : identifier -> bool
-- 
cgit v1.2.3