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 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel/names.ml')

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
-- 
cgit v1.2.3