diff options
| author | Xavier Leroy | 2019-06-24 17:08:11 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-01-08 15:07:15 +0100 |
| commit | bfb28c7720d9101e2caedff0c1f1f2cdbf0bad65 (patch) | |
| tree | efe2b91a00c554e79c17cbaddf2f36b8c0ad24ed /plugins/extraction/ocaml.ml | |
| parent | 3cdbd61f3acf0722c92f8192425eb1a677270b08 (diff) | |
Support extraction of Coq's string type to OCaml's string type
Instead of the default extraction to OCaml's "char list" type.
Diffstat (limited to 'plugins/extraction/ocaml.ml')
| -rw-r--r-- | plugins/extraction/ocaml.ml | 1 |
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) |