diff options
| author | Brian Campbell | 2018-09-12 14:29:23 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-09-12 14:29:23 +0100 |
| commit | f4e1864e63a9f88ba5b175dad3f7c8ca6aab8552 (patch) | |
| tree | 58f99edbbdba56ef20b69bbc187656acfdb3c58d /src | |
| parent | 230621c33a8ce2ef8058d22fda0cd998f621dc65 (diff) | |
Coq: avoid some use of pattern binders to help Coq's type checker
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 12c9ee0e..2b72ef5f 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1470,7 +1470,18 @@ let doc_exp, doc_let = let e1_pp = parens (separate space [expN e1; colon; string (if ctxt.early_ret then "MR" else "M"); parens (doc_typ ctxt typ')]) in - let middle = separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat', typ'); bigarrow] in + let middle = + match pat' with + | P_aux (P_id id,_) + when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) && + not (is_enum (env_of e1) id) -> + separate space [string ">>= fun"; doc_id id; bigarrow] + | P_aux (P_typ (typ, P_aux (P_id id,_)),_) + when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) && + not (is_enum (env_of e1) id) -> + separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] | _ -> + separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat', typ'); bigarrow] + in infix 0 1 middle e1_pp (expN e2') | _ -> let epp = |