diff options
| author | Brian Campbell | 2020-06-17 20:09:08 +0100 |
|---|---|---|
| committer | Brian Campbell | 2020-06-17 20:09:08 +0100 |
| commit | 4ea47e5a20f6cdf201774e8bd2ddfb977ee4dc43 (patch) | |
| tree | 1c2e415b5769342df09645dc64d6f4e797b0aef7 | |
| parent | a7d351c71d43585d789bc92df3ba27f4e533d1b7 (diff) | |
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.
| -rw-r--r-- | src/pretty_print_coq.ml | 8 |
1 files 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 |