diff options
| author | filliatr | 1999-11-19 17:01:43 +0000 |
|---|---|---|
| committer | filliatr | 1999-11-19 17:01:43 +0000 |
| commit | 9bdaa212057cdd41ba416cc9f05167e91eeed4b3 (patch) | |
| tree | 328de03d16931d5abfd9ac4c0254b93cb0e5dcf9 /library | |
| parent | b0382a9829f08282351244839526bd2ffbe6283f (diff) | |
module Pattern, Wcclausenv (interface) et Tacticals
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@126 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 4 | ||||
| -rw-r--r-- | library/declare.mli | 2 |
2 files changed, 3 insertions, 3 deletions
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 |