diff options
| author | Brian Campbell | 2019-05-19 18:39:09 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-05-19 18:40:26 +0100 |
| commit | baf7c57218b37618c5ede4ec72d3c79e9c14cd51 (patch) | |
| tree | bcff2df1239e8dd9d4f5c54f72c8ae22fc25238c /src | |
| parent | cb95f36b485749cb739acea5373745b99332d874 (diff) | |
Coq: remove unhelpful type printing restriction on early returns
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 37e99662..952554a1 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1604,16 +1604,11 @@ let doc_exp, doc_let = | None -> expY exp in let epp = separate space [string "early_return"; exp_pp] in - let aexp_needed, tepp = - if contains_t_pp_var ctxt (typ_of exp) || - contains_t_pp_var ctxt (typ_of full_exp) then - aexp_needed, epp - else - let tannot = separate space [string "MR"; - doc_atomic_typ ctxt (env_of full_exp) false (typ_of full_exp); - doc_atomic_typ ctxt (env_of exp) false (typ_of exp)] in - true, doc_op colon epp tannot in - if aexp_needed then parens tepp else tepp + let tannot = separate space [string "MR"; + doc_atomic_typ ctxt (env_of full_exp) false (typ_of full_exp); + doc_atomic_typ ctxt (env_of exp) false (typ_of exp)] + in + parens (doc_op colon epp tannot) | _ -> raise (Reporting.err_unreachable l __POS__ "Unexpected number of arguments for early_return builtin") end |