From baf7c57218b37618c5ede4ec72d3c79e9c14cd51 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Sun, 19 May 2019 18:39:09 +0100
Subject: Coq: remove unhelpful type printing restriction on early returns

---
 src/pretty_print_coq.ml | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

(limited to 'src')

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
-- 
cgit v1.2.3