From 2cb15665392d0b87da9e0c1f43e19267f28c3a82 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 3 Aug 2018 14:52:44 +0100
Subject: Coq: generalise dependent pair handling a little 1. for monadic
 values (not in a terribly useful way, though) 2. for more types

---
 src/pretty_print_coq.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 93a24f4e..dff68092 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1133,10 +1133,13 @@ let doc_exp_lem, doc_let_lem =
                 | _ -> false
               in unpack,build_ex,autocast
             in
-            let autocast_id = if effectful eff then "autocast_m" else "autocast" in
-            let epp = if unpack then string "projT1" ^^ space ^^ parens epp else epp in
+            let autocast_id, proj_id, build_id =
+              if effectful eff
+              then "autocast_m", "projT1_m", "build_ex_m"
+              else "autocast",   "projT1",   "build_ex" in
+            let epp = if unpack then string proj_id ^^ space ^^ parens epp else epp in
             let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in
-            let epp = if build_ex then string "build_ex" ^^ space ^^ parens epp else epp in
+            let epp = if build_ex then string build_id ^^ space ^^ parens epp else epp in
             liftR (if aexp_needed then parens (align epp) else epp)
        end
     | E_vector_access (v,e) ->
-- 
cgit v1.2.3