From 06c20157840425fb367feb186f009858a3a00448 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 12 Jul 2018 15:52:40 +0100
Subject: Coq: get rid of syntax error on exception handling

---
 src/pretty_print_coq.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/pretty_print_coq.ml')

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
-- 
cgit v1.2.3