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/termops.mli | |
| 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/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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 |