From e9ecc057647d1a13c2eefda0a66a411a6aa17e35 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 5 Apr 2019 10:51:16 +0100
Subject: Coq: add missing effectful existential unpacking case

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

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index cce3c2d3..90484598 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1729,7 +1729,11 @@ let doc_exp, doc_let =
             if effectful eff
             then "autocast_m", "projT1_m"
             else "autocast",   "projT1" in
-          let epp = if unpack && not (effectful eff) then string proj_id ^/^ parens epp else epp in
+          (* We need to unpack an existential if it's generated by a pure
+             computation, or if the monadic binding isn't expecting one. *)
+          let epp = if unpack && not (effectful eff && packeff)
+                    then string proj_id ^/^ parens epp
+                    else epp in
           let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in
           let epp =
             if effectful eff && packeff && not unpack
-- 
cgit v1.2.3