diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-22 14:30:01 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-22 14:30:01 +0000 |
| commit | f6d8fc17dc9474e4d043cf709d672d9259599354 (patch) | |
| tree | 3e05dce982c2bebb63f432064136d927a227e0c7 /printing | |
| parent | 08e7ec2c48c5ca666ad42b5f969576e6aa43d2ea (diff) | |
Nicer code concerning dirpaths and modpath around Lib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index cc9356cda..05037a150 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -144,12 +144,11 @@ let id_of_global env = function (Environ.lookup_mind kn env).mind_packets.(i).mind_consnames.(j-1) | VarRef v -> v -let cons_dirpath id dp = DirPath.make (id :: DirPath.repr dp) - let rec dirpath_of_mp = function | MPfile sl -> sl | MPbound uid -> DirPath.make [MBId.to_id uid] - | MPdot (mp,l) -> cons_dirpath (Label.to_id l) (dirpath_of_mp mp) + | MPdot (mp,l) -> + Libnames.add_dirpath_suffix (dirpath_of_mp mp) (Label.to_id l) let dirpath_of_global = function | ConstRef kn -> dirpath_of_mp (Constant.modpath kn) |