diff options
| author | Brian Campbell | 2018-07-12 15:52:40 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-12 15:52:40 +0100 |
| commit | 06c20157840425fb367feb186f009858a3a00448 (patch) | |
| tree | d1a7ad0f1f24a001160d9b0a2452984ec254bc77 /src/pretty_print_coq.ml | |
| parent | 3e8afd335d1648b700fa04c80312326aec49c9c0 (diff) | |
Coq: get rid of syntax error on exception handling
Diffstat (limited to 'src/pretty_print_coq.ml')
| -rw-r--r-- | src/pretty_print_coq.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 28289241..52ecc715 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1179,7 +1179,8 @@ let doc_exp_lem, doc_let_lem = if effectful (effect_of e) then let try_catch = if ctxt.early_ret then "try_catchR" else "try_catch" in let epp = - group ((separate space [string try_catch; expY e; string "(function "]) ^/^ + (* TODO capture avoidance for __catch_val *) + group ((separate space [string try_catch; expY e; string "(fun __catch_val => match __catch_val with "]) ^/^ (separate_map (break 1) (doc_case ctxt exc_typ) pexps) ^/^ (string "end)")) in if aexp_needed then parens (align epp) else align epp |