diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-17 12:49:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-17 12:49:19 +0000 |
| commit | a6d858b84132bcb27bcc771f06a854cc94eef716 (patch) | |
| tree | df016a77a6d8d2f2a43fa9c2c01adc09b3be7c1b /library/nametab.mli | |
| parent | 000ece141dc22e35365ea81558e8b6b1e65bd54c (diff) | |
Abstraction de l'immplementation de dirpath et implementation dans l'autre sens pour plus de partage entre chemins
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.mli')
| -rwxr-xr-x | library/nametab.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/library/nametab.mli b/library/nametab.mli index 44e4e6b44..5fb7eb237 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -28,6 +28,7 @@ type qualid val make_qualid : dir_path -> identifier -> qualid val repr_qualid : qualid -> dir_path * identifier +val make_short_qualid : identifier -> qualid val string_of_qualid : qualid -> string val pr_qualid : qualid -> std_ppcmds @@ -89,7 +90,7 @@ val coq_root : module_ident val default_root_prefix : dir_path (* This is to declare a new root *) -val push_library_root : module_ident -> unit +val push_library_root : dir_path -> unit (* This turns a "user" absolute name into a global reference; especially, constructor/inductive names are turned into internal |