diff options
| author | Brian Campbell | 2018-05-29 15:44:10 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-08 15:03:37 +0100 |
| commit | 0c02580108effb66c427906e990cf567bdd0ad75 (patch) | |
| tree | 39ca8d545651e4f3ae293afe8e2a10c16fd256c4 /src/pretty_print_coq.ml | |
| parent | 548d02f6667644154c5b5547331e34a278bae22c (diff) | |
Coq: correct failure on unsupported undefined values
Diffstat (limited to 'src/pretty_print_coq.ml')
| -rw-r--r-- | src/pretty_print_coq.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index b0d7cb0e..2742b856 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -412,7 +412,7 @@ let doc_lit (L_aux(lit,l)) = | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*) | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*) | L_undef -> - utf8string "(return (failwith \"undefined value of unsupported type\"))" + utf8string "(Fail \"undefined value of unsupported type\")" | L_string s -> utf8string ("\"" ^ s ^ "\"") | L_real s -> (* Lem does not support decimal syntax, so we translate a string |