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.

6 files changed, 19 insertions, 14 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 858c80f296..b74b1faca0 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -504,8 +504,8 @@ let f_equal =
 	  end
       | _ -> Proofview.tclUNIT ()
       end
-      begin function
+      begin function (e, info) -> match e with
         | Type_errors.TypeError _ -> Proofview.tclUNIT ()
-        | e -> Proofview.tclZERO e
+        | e -> Proofview.tclZERO ~info e
       end
   end
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 43fefc4c6c..c8214ada8e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -74,9 +74,10 @@ let do_observe_tac s tac g =
     ignore(Stack.pop debug_queue);
     v
   with reraise ->
+    let reraise = Errors.push reraise in
     if not (Stack.is_empty debug_queue)
-    then print_debug_queue true (Cerrors.process_vernac_interp_error reraise);
-    raise reraise
+    then print_debug_queue true (fst (Cerrors.process_vernac_interp_error reraise));
+    iraise reraise
 
 let observe_tac_stream s tac g =
   if do_observe ()
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 71da59c499..1051cae75f 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -186,7 +186,7 @@ END
 
 
 let warning_error names e =
-  let e = Cerrors.process_vernac_interp_error e in
+  let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in
   match e with
     | Building_graph e ->
 	Pp.msg_warning
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2ce9f4f616..6dbd61cfdd 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -217,6 +217,8 @@ let prepare_body ((name,_,args,types,_),_) rt =
   let fun_args,rt' = chop_rlambda_n n rt in
   (fun_args,rt')
 
+let process_vernac_interp_error e =
+  fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))
 
 let derive_inversion fix_names =
   try
@@ -243,23 +245,23 @@ let derive_inversion fix_names =
 	   fix_names
 	)
     with e when Errors.noncritical e ->
-      let e' = Cerrors.process_vernac_interp_error e in
+      let e' = process_vernac_interp_error e in
       msg_warning
 	(str "Cannot build inversion information" ++
 	   if do_observe () then (fnl() ++ Errors.print e') else mt ())
   with e when Errors.noncritical e -> ()
 
 let warning_error names e =
-  let e = Cerrors.process_vernac_interp_error e in
+  let e = process_vernac_interp_error e in
   let e_explain e =
     match e with
       | ToShow e -> 
-	let e = Cerrors.process_vernac_interp_error e in
+	let e = process_vernac_interp_error e in
 	spc () ++ Errors.print e
       | _ -> 
 	if do_observe () 
 	then 
-	  let e = Cerrors.process_vernac_interp_error e in 
+	  let e = process_vernac_interp_error e in 
 	  (spc () ++ Errors.print e) 
 	else mt ()
   in
@@ -277,7 +279,7 @@ let warning_error names e =
     | _ -> raise e
 
 let error_error names e =
-  let e = Cerrors.process_vernac_interp_error e in
+  let e = process_vernac_interp_error e in
   let e_explain e =
     match e with
       | ToShow e -> spc () ++ Errors.print e
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index e07bce69c9..8a6c8430fd 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -68,10 +68,11 @@ let do_observe_tac s tac g =
     let v = tac g in
     msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
   with reraise ->
+    let reraise = Errors.push reraise in
     let e = Cerrors.process_vernac_interp_error reraise in
     msgnl (str "observation "++ s++str " raised exception " ++
-	     Errors.print e ++ str " on goal " ++ goal );
-    raise reraise;;
+	     Errors.iprint e ++ str " on goal " ++ goal );
+    iraise reraise;;
 
 
 let observe_tac_strm s tac g =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index a38764c5bd..a466e1089e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -236,9 +236,10 @@ let do_observe_tac s tac g =
     ignore(Stack.pop debug_queue);
     v
   with reraise ->
+    let reraise = Errors.push reraise in
     if not (Stack.is_empty debug_queue)
-    then print_debug_queue true (Cerrors.process_vernac_interp_error reraise);
-    raise reraise
+    then print_debug_queue true (fst (Cerrors.process_vernac_interp_error reraise));
+    iraise reraise
 
 let observe_tac s tac g =
   if do_observe ()