diff options
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 |