diff options
| author | Brian Campbell | 2018-08-09 11:17:46 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-08-09 15:29:28 +0100 |
| commit | 93b8618d2b1c14c58340eae4873632fb4d7c1a20 (patch) | |
| tree | e3f0297ec1236a3d9462850099daeab208ce0740 /src/pretty_print_coq.ml | |
| parent | 07cb99b638d118a23cc8610c6cffbf5834b0fa87 (diff) | |
Coq: decompose dependent pairs at internal_plet as well as let
Diffstat (limited to 'src/pretty_print_coq.ml')
| -rw-r--r-- | src/pretty_print_coq.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 74d10f44..d55e226b 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1315,9 +1315,11 @@ let doc_exp_lem, doc_let_lem = match pat with | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>" - | P_aux (P_id id,_) -> + | P_aux (P_id id,_) + when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) -> separate space [string ">>= fun"; doc_id id; bigarrow] - | P_aux (P_typ (typ, P_aux (P_id id,_)),_) -> + | P_aux (P_typ (typ, P_aux (P_id id,_)),_) + when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) -> 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] |