Getting rid of Exninfo hacks.

Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.

To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.

The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.

1 files changed, 6 insertions, 6 deletions

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 80aaf9f2a9..b25f37b369 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -138,9 +138,9 @@ let rec prompt level =
     Proofview.NonLogical.print (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
     let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
     Proofview.NonLogical.catch Proofview.NonLogical.read_line
-      begin function
+      begin function (e, info) -> match e with
         | End_of_file -> exit
-        | e -> raise e
+        | e -> raise ~info e
       end
     >>= fun inst ->
     match inst with
@@ -154,9 +154,9 @@ let rec prompt level =
       end
     | _ ->
         Proofview.NonLogical.catch (run_com inst >> runtrue >> return (DebugOn (level+1)))
-          begin function
+          begin function (e, info) -> match e with
             | Failure _ | Invalid_argument _ -> prompt level
-            | e -> raise e
+            | e -> raise ~info e
           end
   end
 
@@ -189,7 +189,7 @@ let debug_prompt lev tac f =
   (* What to execute *)
   Proofview.tclOR
     (f newlevel)
-    begin fun reraise ->
+    begin fun (reraise, info) ->
       Proofview.tclTHEN
         (Proofview.tclLIFT begin
           (skip:=0) >> (skipped:=0) >>
@@ -197,7 +197,7 @@ let debug_prompt lev tac f =
               msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ Pervasives.(!) explain_logic_error reraise)
             else return ()
         end)
-        (Proofview.tclZERO reraise)
+        (Proofview.tclZERO ~info reraise)
     end
 
 let is_debug db =