From e6b66c74e01315a6b34223cf328ec600373df658 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 28 May 2019 17:35:05 +0100
Subject: Coq: don't output complex bool types at let expressions

---
 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 af40578c..f1128d7a 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -2226,7 +2226,7 @@ let doc_exp, doc_let =
               (separate space [string "let"; doc_id id; coloneq])
               (top_exp ctxt false e)
     | LB_val(P_aux (P_typ (typ,P_aux (P_id id,_)),_),e)
-      when Util.is_none (is_auto_decomposed_exist ctxt (env_of e) typ) &&
+      when Util.is_none (is_auto_decomposed_exist ctxt (env_of e) ~rawbools:true typ) &&
            not (is_enum (env_of e) id) ->
        prefix 2 1
               (separate space [string "let"; doc_id id; colon; doc_typ ctxt (env_of e) typ; coloneq])
-- 
cgit v1.2.3