aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/ocaml.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/ocaml.ml')
-rw-r--r--plugins/extraction/ocaml.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 66429833b9..ab37bd2d76 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -249,6 +249,7 @@ let rec pp_expr par env args =
assert (List.is_empty args);
begin match a with
| _ when is_native_char c -> pp_native_char c
+ | _ when is_native_string c -> pp_native_string c
| [a1;a2] when is_infix r ->
let pp = pp_expr true env [] in
pp_par par (pp a1 ++ str (get_infix r) ++ pp a2)