From 693d398b5e4e55a916bbdaa8e4c23c83d9dbcef7 Mon Sep 17 00:00:00 2001
From: notin
Date: Wed, 25 Jun 2008 18:19:21 +0000
Subject: Création du fichier dumpglob.ml, qui rassemble les fonctions de
 globalisation (add_glob* et dump_*)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/names.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/names.mli')

diff --git a/kernel/names.mli b/kernel/names.mli
index b19f93e2d9..177768cf43 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -48,6 +48,7 @@ type mod_self_id
 (* The first argument is a file name - to prevent conflict between 
    different files *)
 val make_msid : dir_path -> string -> mod_self_id
+val repr_msid : mod_self_id -> int * string * dir_path
 val id_of_msid : mod_self_id -> identifier
 val label_of_msid : mod_self_id -> label
 val refresh_msid : mod_self_id -> mod_self_id
@@ -58,6 +59,7 @@ val string_of_msid : mod_self_id -> string
 type mod_bound_id
 
 val make_mbid : dir_path -> string -> mod_bound_id
+val repr_mbid : mod_bound_id -> int * string * dir_path
 val id_of_mbid : mod_bound_id -> identifier
 val label_of_mbid : mod_bound_id -> label
 val debug_string_of_mbid : mod_bound_id -> string
@@ -82,7 +84,6 @@ type module_path =
   | MPdot of module_path * label
 (*i  | MPapply of module_path * module_path    in the future (maybe) i*)
 
-
 val string_of_mp : module_path -> string
 
 module MPset : Set.S with type elt = module_path
-- 
cgit v1.2.3