diff options
| author | Brian Campbell | 2018-06-22 10:57:52 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-22 15:26:32 +0100 |
| commit | 91fa030034661953f2299a41c31fb7647288b4cb (patch) | |
| tree | 032323e0b9c61a19e4eb5e2b764fc0f200eae19c /src | |
| parent | 3d8609d963ee411f777ba18dc24fe57bf39dcaab (diff) | |
Coq: use simple forms for simple pattern matches in E_internal_let
Diffstat (limited to 'src')
| -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 |