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.ml  | 4 +++-
 kernel/names.mli | 3 ++-
 2 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index 975390cb9e..3d80ad23e8 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -86,6 +86,7 @@ type label = string
 
 type mod_self_id = uniq_ident
 let make_msid = make_uid
+let repr_msid (n, id, dp) = (n, id, dp)
 let debug_string_of_msid = debug_string_of_uid
 let refresh_msid (_,s,dir) = make_uid dir s
 let string_of_msid = string_of_uid
@@ -94,6 +95,7 @@ let label_of_msid (_,s,_) = s
 
 type mod_bound_id = uniq_ident
 let make_mbid = make_uid
+let repr_mbid (n, id, dp) = (n, id, dp)
 let debug_string_of_mbid = debug_string_of_uid
 let string_of_mbid = string_of_uid
 let id_of_mbid (_,s,_) = s
@@ -116,7 +118,7 @@ type module_path =
   | MPdot of module_path * label
 
 let rec string_of_mp = function
-  | MPfile sl -> string_of_dirpath sl
+  | MPfile sl -> "MPfile (" ^ string_of_dirpath sl ^ ")"
   | MPbound uid -> string_of_uid uid
   | MPself uid -> string_of_uid uid
   | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
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