From 4ea47e5a20f6cdf201774e8bd2ddfb977ee4dc43 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 17 Jun 2020 20:09:08 +0100
Subject: Coq: fix rich loop variables Accidentally broken by e1a2b0d2 because
 the Coq backend looks at the wrong type to decide when a proof is needed.

---
 src/pretty_print_coq.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index d0d13907..dbb0356d 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1620,8 +1620,10 @@ let doc_exp, doc_let =
                let from_exp_pp, to_exp_pp, step_exp_pp =
                  expY from_exp, expY to_exp, expY step_exp
                in
+               (* The body has the right type for deciding whether a proof is necessary *)
+               let vartuple_retyped = check_exp env (strip_exp vartuple) (general_typ_of body) in
                let vartuple_pp, body_lambda =
-                 make_loop_vars [doc_id loopvar; underscore] vartuple
+                 make_loop_vars [doc_id loopvar; underscore] vartuple_retyped
                in
                parens (
                    (prefix 2 1)
@@ -1673,8 +1675,10 @@ let doc_exp, doc_let =
               | _ -> body
             in
             let used_vars_body = find_e_ids body in
+            (* The body has the right type for deciding whether a proof is necessary *)
+            let varstuple_retyped = check_exp env (strip_exp varstuple) (general_typ_of body) in
             let varstuple_pp, lambda =
-              make_loop_vars [] varstuple
+              make_loop_vars [] varstuple_retyped
             in
             let msuffix, measure_pp =
               match measure with
-- 
cgit v1.2.3