diff options
| author | filliatr | 2000-04-28 17:56:13 +0000 |
|---|---|---|
| committer | filliatr | 2000-04-28 17:56:13 +0000 |
| commit | 7a7fff7bd838d2c54cf341549c5b0e1d3cf21803 (patch) | |
| tree | 2dd9530bc92aa339da6ed9cd3d0b40c078926c88 /library | |
| parent | 44d578b40ec699ea8bbd4b387c2cf7155bf1d1fe (diff) | |
portage Omega (code seulement)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@381 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |