From a6d858b84132bcb27bcc771f06a854cc94eef716 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 17 Oct 2001 12:49:19 +0000 Subject: 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 --- library/nametab.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'library/nametab.mli') 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 -- cgit v1.2.3