aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/ocaml.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 /plugins/extraction/ocaml.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 'plugins/extraction/ocaml.ml')
-rw-r--r--plugins/extraction/ocaml.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 7742dd783..fbd3fd4ea 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -648,9 +648,9 @@ and pp_module_type params = function
let mp_mt = msid_of_mt mt in
let l,idl' = List.sep_last idl in
let mp_w =
- List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
+ List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
in
- let r = ConstRef (make_con mp_w Dir_path.empty (label_of_id l)) in
+ let r = ConstRef (make_con mp_w Dir_path.empty (Label.of_id l)) in
push_visible mp_mt [];
let pp_w = str " with type " ++ ids ++ pp_global Type r in
pop_visible();
@@ -658,7 +658,7 @@ and pp_module_type params = function
| MTwith(mt,ML_With_module(idl,mp)) ->
let mp_mt = msid_of_mt mt in
let mp_w =
- List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl
+ List.fold_left (fun mp id -> MPdot(mp,Label.of_id id)) mp_mt idl
in
push_visible mp_mt [];
let pp_w = str " with module " ++ pp_modname mp_w in