with @mtzguido, fixing Errors.catch_errors_aux, so that it finally re…

…stores the original error handler

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 ();

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)