From 542533ac7cbef0377de8413c3ac84c6fff2b9964 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 5 Mar 2019 12:16:17 +0000
Subject: Coq: use more local type information when constructing tuples

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

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 5dab3b8e..fe94dbb5 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1200,11 +1200,12 @@ let doc_exp, doc_let =
          wrap_parens (string "build_ex" ^/^ epp)
     in
     let construct_dep_pairs ?(rawbools=false) env =
-      let rec aux want_parens (E_aux (e,_) as exp) (Typ_aux (t,_) as typ) =
-        match e,t with
-        | E_tuple exps, Typ_tup typs
-        | E_cast (_, E_aux (E_tuple exps,_)), Typ_tup typs
+      let rec aux want_parens (E_aux (e,_) as exp) typ =
+        match e with
+        | E_tuple exps
+        | E_cast (_, E_aux (E_tuple exps,_))
           ->
+           let typs = List.map general_typ_of exps in
            parens (separate (string ", ") (List.map2 (aux false) exps typs))
         | _ ->
            let typ' = expand_range_type (Env.expand_synonyms (env_of exp) typ) in
-- 
cgit v1.2.3