diff options
| author | Brian Campbell | 2019-03-05 12:16:17 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-03-05 12:16:17 +0000 |
| commit | 542533ac7cbef0377de8413c3ac84c6fff2b9964 (patch) | |
| tree | 85c7f0949593c21658d6d4f64f1e1a35223302fd /src | |
| parent | 8e8684e97e063912e53fdcade132051f09304d55 (diff) | |
Coq: use more local type information when constructing tuples
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 9 |
1 files changed, 5 insertions, 4 deletions
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 |