diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 13 | ||||
| -rw-r--r-- | library/declare.mli | 2 |
2 files changed, 12 insertions, 3 deletions
diff --git a/library/declare.ml b/library/declare.ml index 51748a0204..2ccd77cf09 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -238,8 +238,7 @@ let construct_operator env sp id = let global_operator sp id = construct_operator (Global.env()) sp id -let construct_reference env kind id = - let sp = Nametab.sp_of_id kind id in +let construct_sp_reference env sp id = try let (oper,hyps) = construct_operator env sp id in let hyps' = Global.var_context () in @@ -250,7 +249,15 @@ let construct_reference env kind id = with Not_found -> VAR (let _ = Environ.lookup_var id env in id) -let global_reference kind id = construct_reference (Global.env()) kind id +let construct_reference env kind id = + let sp = Nametab.sp_of_id kind id in + construct_sp_reference env sp id + +let global_sp_reference sp id = + construct_sp_reference (Global.env()) sp id + +let global_reference kind id = + construct_reference (Global.env()) kind id let global_reference_imps kind id = let c = global_reference kind id in diff --git a/library/declare.mli b/library/declare.mli index 470d6dee9d..0142eb0ac6 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -65,6 +65,8 @@ val global_operator : section_path -> identifier -> sorts oper * var_context [construct_reference] is a version which looks for variables in a given environment instead of looking in the current global environment. *) +val global_sp_reference : section_path -> identifier -> constr + val global_reference : path_kind -> identifier -> constr val global_reference_imps : path_kind -> identifier -> constr * int list |