diff options
| -rw-r--r-- | src/pretty_print_coq.ml | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 09cbbecf..2b328ecb 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1089,14 +1089,10 @@ let doc_exp_lem, doc_let_lem = match fst (untyp_pat pat) with | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>" - | P_aux (P_tup _, _) - when not (IdSet.mem (mk_id "varstup") (find_e_ids e2)) -> - (* Work around indentation issues in Lem when translating - tuple patterns to Isabelle *) - separate space - [string ">>= fun varstup => let"; - doc_pat ctxt true (pat, typ_of e1); - string ":= varstup in"] + | P_aux (P_id id,_) -> + separate space [string ">>= fun"; doc_id id; bigarrow] + | P_aux (P_typ (typ, P_aux (P_id id,_)),_) -> + 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] in |