From 6946bbbf2390024b3ded7654814104e709cce755 Mon Sep 17 00:00:00 2001 From: ppedrot 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/lib.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'library/lib.ml') diff --git a/library/lib.ml b/library/lib.ml index 9ac9b7c71..0f2f480cb 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -658,13 +658,13 @@ let rec split_mp mp = | Names.MPdot (prfx, lbl) -> let mprec, dprec = split_mp prfx in mprec, Names.Dir_path.make (Names.Id.of_string (Names.Label.to_string lbl) :: (Names.Dir_path.repr dprec)) - | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.Dir_path.make [id] + | Names.MPbound mbid -> let (_, id, dp) = Names.MBId.repr mbid in library_dp(), Names.Dir_path.make [id] let split_modpath mp = let rec aux = function | Names.MPfile dp -> dp, [] | Names.MPbound mbid -> - library_dp (), [Names.id_of_mbid mbid] + library_dp (), [Names.MBId.to_id mbid] | Names.MPdot (mp,l) -> let (mp', lab) = aux mp in (mp', Names.Label.to_id l :: lab) in -- cgit v1.2.3