From 38ba8e269bbce49cbcb0c09205a9f11df8a538f6 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 20 Jun 2018 14:40:23 +0100
Subject: Coq: add missing existential projection on simple let expressions

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

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 2e07dea7..e9deaea2 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1140,7 +1140,8 @@ let doc_exp_lem, doc_let_lem =
   and let_exp ctxt (LB_aux(lb,_)) = match lb with
     (* Prefer simple lets over patterns, because I've found Coq can struggle to
        work out return types otherwise *)
-    | LB_val(P_aux (P_id id,_),e) ->
+    | LB_val(P_aux (P_id id,_),e)
+      when Util.is_none (is_auto_decomposed_exist (env_of e) (typ_of e)) ->
        prefix 2 1
               (separate space [string "let"; doc_id id; coloneq])
               (top_exp ctxt false e)
-- 
cgit v1.2.3