From 93b8618d2b1c14c58340eae4873632fb4d7c1a20 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 9 Aug 2018 11:17:46 +0100
Subject: Coq: decompose dependent pairs at internal_plet as well as let

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

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 74d10f44..d55e226b 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1315,9 +1315,11 @@ let doc_exp_lem, doc_let_lem =
                 match pat with
                 | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) ->
                    string ">>"
-                | P_aux (P_id id,_) ->
+                | P_aux (P_id id,_)
+                   when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) ->
                    separate space [string ">>= fun"; doc_id id; bigarrow]
-                | P_aux (P_typ (typ, P_aux (P_id id,_)),_) ->
+                | P_aux (P_typ (typ, P_aux (P_id id,_)),_)
+                   when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) ->
                    separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow]
                 | _ ->
                    separate space [string ">>= fun"; squote ^^ doc_pat ctxt true (pat, typ_of e1); bigarrow]
-- 
cgit v1.2.3