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/tactics/equality.ml b/tactics/equality.ml
index 5361125538..9740f6c1f8 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -223,10 +223,10 @@ let general_elim_clause with_evars frzevars cls rew elim =
       tclNOTSAMEGOAL (rewrite_elim with_evars frzevars cls rew elim)
     | Some _ -> rewrite_elim with_evars frzevars cls rew elim
     end
-    begin function
+    begin function (e, info) -> match e with
     | PretypeError (env, evd, NoOccurrenceFound (c', _)) ->
       Proofview.tclZERO (PretypeError (env, evd, NoOccurrenceFound (c', cls)))
-    | e -> Proofview.tclZERO e
+    | e -> Proofview.tclZERO ~info e
     end
 
 let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
@@ -394,7 +394,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
 				   lft2rgt occs (c,l) ~new_goals:[]) tac
             end
             begin function
-              | e ->
+              | (e, info) ->
 	          let env' = push_rel_context rels env in
 	          let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
 	          match match_with_equality_type t' with
@@ -402,7 +402,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
 		  let lft2rgt = adjust_rewriting_direction args lft2rgt in
 		  leibniz_rewrite_ebindings_clause cls lft2rgt tac c
 		    (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok hdcncl
-	            | None -> Proofview.tclZERO e
+	            | None -> Proofview.tclZERO ~info e
             (* error "The provided term does not end with an equality or a declared rewrite relation." *)  
             end
     end
@@ -1507,7 +1507,7 @@ let cutSubstInHyp l2r eqn id =
   end
 
 let try_rewrite tac =
-  Proofview.tclORELSE tac begin function
+  Proofview.tclORELSE tac begin function (e, info) -> match e with
     | ConstrMatching.PatternMatchingFailure ->
 	tclZEROMSG (str "Not a primitive equality here.")
     | e when catchable_exception e ->
@@ -1516,7 +1516,7 @@ let try_rewrite tac =
     | NothingToRewrite ->
 	tclZEROMSG
           (strbrk "Nothing to rewrite.")
-    | e -> Proofview.tclZERO e
+    | e -> Proofview.tclZERO ~info e
   end
 
 let cutSubstClause l2r eqn cls =