From 9bdaa212057cdd41ba416cc9f05167e91eeed4b3 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 19 Nov 1999 17:01:43 +0000
Subject: module Pattern, Wcclausenv (interface) et Tacticals

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

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index d9d55da7a6..f92cc43a8d 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -165,8 +165,8 @@ let global_operator sp id =
     let mib = Global.lookup_mind sp in
     mind_oper_of_id sp id mib
 
-let global_reference id =
-  let sp = Nametab.sp_of_id CCI id in
+let global_reference kind id =
+  let sp = Nametab.sp_of_id kind id in
   let oper = global_operator sp id in
   let hyps = get_globals (Global.context ()) in
   let ids =  ids_of_sign hyps in
diff --git a/library/declare.mli b/library/declare.mli
index 2cb576cf1a..3a1e7884fb 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -34,6 +34,6 @@ val declare_mind : mutual_inductive_entry -> unit
   then constructs the corresponding term, associated to the current 
   environment of variables. *)
 
-val global_reference : identifier -> constr
+val global_reference : path_kind -> identifier -> constr
 
 val mind_path : constr -> section_path
-- 
cgit v1.2.3