diff options
| -rw-r--r-- | src/pretty_print_coq.ml | 7 | ||||
| -rw-r--r-- | src/rewrites.ml | 11 |
2 files changed, 17 insertions, 1 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 806234d6..99d63b55 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -694,6 +694,13 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty List.map (subst_unifiers unifiers) arg_typs | _ -> assert false in + (* Constructors that were specified without a return type might get + an extra tuple in their type; expand that here if necessary. + TODO: this should go away if we enforce proper arities. *) + let arg_typs = match pats, arg_typs with + | _::_::_, [Typ_aux (Typ_tup typs,_)] -> typs + | _,_ -> arg_typs + in let ppp = doc_unop (doc_id_ctor id) (parens (separate_map comma (doc_pat ctxt true true) (List.combine pats arg_typs))) in if apat_needed then parens ppp else ppp diff --git a/src/rewrites.ml b/src/rewrites.ml index cdb15717..c470d906 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4595,7 +4595,16 @@ let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat = (match res_pat with | RP_app (id',residual_args) -> if Id.compare id id' == 0 then - let res_pats' = subpats args residual_args in + let res_pats' = + (* Constructors that were specified without a return type might get + an extra tuple in their type; expand that here if necessary. + TODO: this should go away if we enforce proper arities. *) + match args, residual_args with + | [], [RP_any] + | _::_::_, [RP_any] + -> subpats args (List.map (fun _ -> RP_any) args) + | _,_ -> + subpats args residual_args in List.map (fun rps -> RP_app (id,rps)) res_pats' else [res_pat] | RP_any -> |