diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-18 18:05:56 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-18 18:05:56 +0000 |
| commit | 6946bbbf2390024b3ded7654814104e709cce755 (patch) | |
| tree | 643429de27ef09026b937c18a55075eb49b11fee /library/lib.ml | |
| parent | aa37087b8e7151ea96321a11012c1064210ef4ea (diff) | |
Modulification of mod_bound_id
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16098 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |