From 0c02580108effb66c427906e990cf567bdd0ad75 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 29 May 2018 15:44:10 +0100
Subject: Coq: correct failure on unsupported undefined values

---
 src/pretty_print_coq.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

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
-- 
cgit v1.2.3