From 6946bbbf2390024b3ded7654814104e709cce755 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 18 Dec 2012 18:05:56 +0000
Subject: Modulification of mod_bound_id

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16098 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/globnames.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library/globnames.ml')

diff --git a/library/globnames.ml b/library/globnames.ml
index c37e370a3..ea002ef58 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -146,8 +146,8 @@ let decode_mind kn =
   let rec dir_of_mp = function
     | MPfile dir -> Dir_path.repr dir
     | MPbound mbid ->
-	let _,_,dp = repr_mbid mbid in
-	let id = id_of_mbid mbid in
+	let _,_,dp = MBId.repr mbid in
+	let id = MBId.to_id mbid in
 	  id::(Dir_path.repr dp)
     | MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp)
   in
-- 
cgit v1.2.3