diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 2e62188d..163cd183 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -556,6 +556,10 @@ let doc_tannot ctxt env eff typ = else string " : " ^^ ta in of_typ typ +(* Only double-quotes need escaped - by doubling them. *) +let coq_escape_string s = + Str.global_replace (Str.regexp "\"") "\"\"" s + let doc_lit (L_aux(lit,l)) = match lit with | L_unit -> utf8string "tt" @@ -570,7 +574,7 @@ let doc_lit (L_aux(lit,l)) = | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*) | L_undef -> utf8string "(Fail \"undefined value of unsupported type\")" - | L_string s -> utf8string ("\"" ^ s ^ "\"") + | L_string s -> utf8string ("\"" ^ (coq_escape_string s) ^ "\"") | L_real s -> (* Lem does not support decimal syntax, so we translate a string of the form "x.y" into the ratio (x * 10^len(y) + y) / 10^len(y). |