From 4f939658df5f45026d42491b8bf78aaa44f76e7b Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 12 Jul 2018 13:41:07 +0100 Subject: Coq: tuple matching in loops --- src/pretty_print_coq.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index e57238f6..6cb97d5b 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -879,7 +879,7 @@ let doc_exp_lem, doc_let_lem = when not (IdSet.mem (mk_id "varstup") used_vars_body)-> separate space [string "fun"; doc_id loopvar; string "_"; string "varstup"; bigarrow] ^^ break 1 ^^ - separate space [string "let"; expY vartuple; string ":= varstup in"] + separate space [string "let"; squote ^^ expY vartuple; string ":= varstup in"] | E_aux (E_lit (L_aux (L_unit, _)), _) when not (IdSet.mem (mk_id "unit_var") used_vars_body) -> separate space [string "fun"; doc_id loopvar; string "_"; string "unit_var"; bigarrow] @@ -918,7 +918,7 @@ let doc_exp_lem, doc_let_lem = | E_aux (E_tuple _, _) when not (IdSet.mem (mk_id "varstup") used_vars_body)-> separate space [string "fun varstup"; bigarrow] ^^ break 1 ^^ - separate space [string "let"; expY varstuple; string ":= varstup in"] + separate space [string "let"; squote ^^ expY varstuple; string ":= varstup in"] | E_aux (E_lit (L_aux (L_unit, _)), _) when not (IdSet.mem (mk_id "unit_var") used_vars_body) -> separate space [string "fun unit_var"; bigarrow] -- cgit v1.2.3