From f4e1864e63a9f88ba5b175dad3f7c8ca6aab8552 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 12 Sep 2018 14:29:23 +0100
Subject: Coq: avoid some use of pattern binders to help Coq's type checker

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

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 12c9ee0e..2b72ef5f 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1470,7 +1470,18 @@ let doc_exp, doc_let =
             let e1_pp = parens (separate space [expN e1; colon;
                                                 string (if ctxt.early_ret then "MR" else "M");
                                                 parens (doc_typ ctxt typ')]) in
-            let middle = separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat', typ'); bigarrow] in
+            let middle =
+              match pat' with
+              | P_aux (P_id id,_)
+                   when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) &&
+                          not (is_enum (env_of e1) id) ->
+                 separate space [string ">>= fun"; doc_id id; bigarrow]
+              | P_aux (P_typ (typ, P_aux (P_id id,_)),_)
+                   when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) &&
+                          not (is_enum (env_of e1) id) ->
+                 separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow]              | _ ->
+                 separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat', typ'); bigarrow]
+            in
             infix 0 1 middle e1_pp (expN e2')
          | _ ->
             let epp =
-- 
cgit v1.2.3