diff --git a/ocaml/fstar-lib/generated/FStar_Errors.ml b/ocaml/fstar-lib/generated/FStar_Errors.ml
index 74517450383..3e09a6991a6 100644
--- a/ocaml/fstar-lib/generated/FStar_Errors.ml
+++ b/ocaml/fstar-lib/generated/FStar_Errors.ml
@@ -785,19 +785,28 @@ let catch_errors_aux :
     let newh = mk_default_handler false in
     let old = FStar_Compiler_Effect.op_Bang current_handler in
     FStar_Compiler_Effect.op_Colon_Equals current_handler newh;
-    (let r =
+    (let finally_restore uu___1 =
+       let all_issues = newh.eh_report () in
+       FStar_Compiler_Effect.op_Colon_Equals current_handler old;
+       (let uu___3 =
+          FStar_Compiler_List.partition (fun i -> i.issue_level = EError)
+            all_issues in
+        match uu___3 with | (errs, rest) -> (errs, rest)) in
+     let r =
        try
          (fun uu___1 ->
             match () with
             | () -> let uu___2 = f () in FStar_Pervasives_Native.Some uu___2)
            ()
-       with | uu___1 -> (err_exn uu___1; FStar_Pervasives_Native.None) in
-     let all_issues = newh.eh_report () in
-     FStar_Compiler_Effect.op_Colon_Equals current_handler old;
-     (let uu___2 =
-        FStar_Compiler_List.partition (fun i -> i.issue_level = EError)
-          all_issues in
-      match uu___2 with | (errs, rest) -> (errs, rest, r)))
+       with
+       | uu___1 ->
+           if handleable uu___1
+           then (err_exn uu___1; FStar_Pervasives_Native.None)
+           else
+             (let uu___2 = finally_restore () in
+              FStar_Compiler_Effect.raise uu___1) in
+     let uu___1 = finally_restore () in
+     match uu___1 with | (errs, rest) -> (errs, rest, r))
 let no_ctx : 'a . (unit -> 'a) -> 'a =
   fun f ->
     let save = error_context.get () in
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Basic.ml
index aded4c4df3c..0f366d19882 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_Basic.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_Basic.ml
@@ -7162,7 +7162,25 @@ let refl_typing_builtin_wrapper :
   =
   fun f ->
     let tx = FStar_Syntax_Unionfind.new_transaction () in
-    let uu___ = FStar_Errors.catch_errors_and_ignore_rest f in
+    let uu___ =
+      try
+        (fun uu___1 ->
+           match () with | () -> FStar_Errors.catch_errors_and_ignore_rest f)
+          ()
+      with
+      | uu___1 ->
+          let issue =
+            let uu___2 = FStar_Compiler_Util.print_exn uu___1 in
+            let uu___3 = FStar_Errors.get_ctx () in
+            {
+              FStar_Errors.issue_msg = uu___2;
+              FStar_Errors.issue_level = FStar_Errors.EError;
+              FStar_Errors.issue_range = FStar_Pervasives_Native.None;
+              FStar_Errors.issue_number =
+                (FStar_Pervasives_Native.Some (Prims.of_int (17)));
+              FStar_Errors.issue_ctx = uu___3
+            } in
+          ([issue], FStar_Pervasives_Native.None) in
     match uu___ with
     | (errs, r) ->
         (FStar_Syntax_Unionfind.rollback tx;
diff --git a/src/basic/FStar.Errors.fst b/src/basic/FStar.Errors.fst
index e47c42ffeca..834d91c95ad 100644
--- a/src/basic/FStar.Errors.fst
+++ b/src/basic/FStar.Errors.fst
@@ -472,14 +472,24 @@ let catch_errors_aux (f : unit -> 'a) : list issue & list issue & option 'a =
   let newh = mk_default_handler false in
   let old = !current_handler in
   current_handler := newh;
+  let finally_restore () =
+    let all_issues = newh.eh_report() in //de-duplicated already
+    current_handler := old;
+    let errs, rest = List.partition (fun i -> i.issue_level = EError) all_issues in
+    errs, rest
+  in
   let r = try Some (f ())
-          with | ex -> err_exn ex; None
+          with
+          | ex when handleable ex ->
+            err_exn ex;
+            None
+          | ex ->
+            let _ = finally_restore() in
+            raise ex
   in
-  let all_issues = newh.eh_report() in //de-duplicated already
-  current_handler := old;
-  let errs, rest = List.partition (fun i -> i.issue_level = EError) all_issues in
+  let errs, rest = finally_restore() in
   errs, rest, r
-
+ 
 let no_ctx (f : unit -> 'a) : 'a =
   let save = error_context.get () in
   error_context.clear ();
diff --git a/src/tactics/FStar.Tactics.Basic.fst b/src/tactics/FStar.Tactics.Basic.fst
index 187de62ecb1..7676847b448 100644
--- a/src/tactics/FStar.Tactics.Basic.fst
+++ b/src/tactics/FStar.Tactics.Basic.fst
@@ -2272,7 +2272,18 @@ let dbg_refl (g:env) (msg:unit -> string) =
 let issues = list Errors.issue
 let refl_typing_builtin_wrapper (f:unit -> 'a) : tac (option 'a & issues) =
   let tx = UF.new_transaction () in
-  let errs, r = Errors.catch_errors_and_ignore_rest f in
+  let errs, r = 
+    try Errors.catch_errors_and_ignore_rest f
+    with exn -> //catch everything
+      let issue = FStar.Errors.({
+        issue_msg = BU.print_exn exn;
+        issue_level = EError;
+        issue_range = None;
+        issue_number = (Some 17);
+        issue_ctx = get_ctx ()
+      }) in
+      [issue], None
+  in
   UF.rollback tx;
   if List.length errs > 0
   then ret (None, errs)