diff options
| author | Maxime Dénès | 2015-01-23 14:22:53 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-01-23 14:22:53 +0100 |
| commit | 87106cd6a0e613fc61943959d8fc7d3ff025fc5d (patch) | |
| tree | 0bbcb291dc6cde03707e615024c6d3090186c8c2 /plugins | |
| parent | c2d053c6f38a54e3083c8726eccb3e73942107b7 (diff) | |
| parent | 4f632721be8b083126f49dd900a3294521879ec4 (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/ocaml.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 30ac3d3f89..ce88ea6d29 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -634,7 +634,10 @@ and pp_module_type params = function str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MTsig (mp, sign) -> push_visible mp params; - let l = List.map pp_specif sign in + let try_pp_specif x l = + try pp_specif x :: l with Failure "empty phrase" -> l + in + let l = List.fold_right try_pp_specif sign [] in pop_visible (); str "sig " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ @@ -707,7 +710,10 @@ and pp_module_expr params = function str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MEstruct (mp, sel) -> push_visible mp params; - let l = List.map pp_structure_elem sel in + let try_pp_structure_elem x l = + try pp_structure_elem x :: l with Failure "empty phrase" -> l + in + let l = List.fold_right try_pp_structure_elem sel [] in pop_visible (); str "struct " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ |