diff options
| author | Brian Campbell | 2018-07-12 13:41:07 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-12 13:41:07 +0100 |
| commit | 4f939658df5f45026d42491b8bf78aaa44f76e7b (patch) | |
| tree | 3447daed368019f96401de77db64cb35b774f5c9 /src | |
| parent | d3c75495194f810a89d10fede3ea377074af6f53 (diff) | |
Coq: tuple matching in loops
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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] |