diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-13 10:34:26 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-13 10:34:26 +0000 |
| commit | 2a4ea1915c391ba39b99e4fb17d8354278eec212 (patch) | |
| tree | 718b0519f71a8db5802c8ba7121b70109dbf7412 /pretyping | |
| parent | 87466277171441cd541230f03715fb000a38e70e (diff) | |
Deplacement de Declare vers Termops
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4396 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/termops.ml | 2 | ||||
| -rw-r--r-- | pretyping/termops.mli | 1 |
2 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index a1d07777b..6cf9b4e0d 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -865,4 +865,6 @@ let construct_reference ctx id = with Not_found -> global_reference id +let global_reference_in_absolute_module dir id = + constr_of_reference (Nametab.absolute_reference (Libnames.make_path dir id)) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 9c9243c8c..9031ec42d 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -180,6 +180,7 @@ val global_vars_set_of_decl : env -> named_declaration -> Idset.t val construct_reference : named_context -> identifier -> constr val global_reference : identifier -> constr +val global_reference_in_absolute_module : dir_path -> identifier -> constr (* Test if an identifier is the basename of a global reference *) val is_global : identifier -> bool |