aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printmod.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-18 17:09:31 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-18 17:09:31 +0000
commitaa37087b8e7151ea96321a11012c1064210ef4ea (patch)
treefff9ed837668746545832e3bd9f0a6dd99936ee4 /printing/printmod.ml
parentf61e682857596f0274b956295efd2bfba63bc8c0 (diff)
Modulification of Label
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing/printmod.ml')
-rw-r--r--printing/printmod.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 7ee5b92de..039d3ec43 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -90,7 +90,7 @@ let nametab_register_body mp fp (l,body) =
| SFBmodule _ -> () (* TODO *)
| SFBmodtype _ -> () (* TODO *)
| SFBconst _ ->
- push (id_of_label l) (ConstRef (make_con mp Dir_path.empty l))
+ push (Label.to_id l) (ConstRef (make_con mp Dir_path.empty l))
| SFBmind mib ->
let mind = make_mind mp Dir_path.empty l in
Array.iteri
@@ -101,7 +101,7 @@ let nametab_register_body mp fp (l,body) =
mib.mind_packets
let print_body is_impl env mp (l,body) =
- let name = str (string_of_label l) in
+ let name = str (Label.to_string l) in
hov 2 (match body with
| SFBmodule _ -> str "Module " ++ name
| SFBmodtype _ -> str "Module Type " ++ name