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, 11 insertions, 11 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 82ec15559..5c899aefc 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -300,11 +300,11 @@ module New = struct
 
   let tclZEROMSG ?loc msg =
     let err = UserError ("", msg) in
-    let err = match loc with
-    | None -> err
-    | Some loc -> Loc.add_loc err loc
+    let info = match loc with
+    | None -> Exninfo.null
+    | Some loc -> Loc.add_loc Exninfo.null loc
     in
-    tclZERO err
+    tclZERO ~info err
 
   let catch_failerror e =
     try
@@ -362,14 +362,14 @@ module New = struct
       t1 <*>
         Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *)
           begin tclEXTEND (Array.to_list l1) repeat (Array.to_list l2) end
-          begin function
+          begin function (e, info) -> match e with
             | SizeMismatch (i,_)->
                 let errmsg =
                   str"Incorrect number of goals" ++ spc() ++
                   str"(expected "++int i++str(String.plural i " tactic") ++ str")"
                 in
                 tclFAIL 0 errmsg
-            | reraise -> tclZERO reraise
+            | reraise -> tclZERO ~info reraise
           end
     end
   let tclTHENSFIRSTn t1 l repeat =
@@ -385,14 +385,14 @@ module New = struct
     tclINDEPENDENT begin
       t <*>Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *)
           begin tclDISPATCH l end
-          begin function
+          begin function (e, info) -> match e with
             | SizeMismatch (i,_)->
                 let errmsg =
                   str"Incorrect number of goals" ++ spc() ++
                   str"(expected "++int i++str(String.plural i " tactic") ++ str")"
                 in
                 tclFAIL 0 errmsg
-            | reraise -> tclZERO reraise
+            | reraise -> tclZERO ~info reraise
           end
     end
   let tclTHENLIST l =
@@ -410,7 +410,7 @@ module New = struct
     tclINDEPENDENT begin
       Proofview.tclIFCATCH t1
         (fun () -> t2)
-        (fun e -> Proofview.tclORELSE t3 (fun e' -> tclZERO e))
+        (fun (e, info) -> Proofview.tclORELSE t3 (fun e' -> tclZERO ~info e))
     end
   let tclIFTHENSVELSE t1 a t3 =
     Proofview.tclIFCATCH t1
@@ -519,9 +519,9 @@ module New = struct
   let tclTIMEOUT n t =
     Proofview.tclOR
       (Proofview.tclTIMEOUT n t)
-      begin function
+      begin function (e, info) -> match e with
         | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (Errors.print e)))
-        | e -> Proofview.tclZERO e
+        | e -> Proofview.tclZERO ~info e
       end
 
   let tclTIME s t =