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.

14 files changed, 110 insertions, 102 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 43aa84e7ae..ef6c38bf6c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -205,7 +205,7 @@ let tclLOG (dbg,depth,trace) pp tac =
 	with reraise ->
           let reraise = Errors.push reraise in
 	  msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
-	  raise reraise
+	  iraise reraise
       end
     | Info ->
       (* For "info (trivial/auto)", we store a log trace *)
@@ -217,7 +217,7 @@ let tclLOG (dbg,depth,trace) pp tac =
 	with reraise ->
           let reraise = Errors.push reraise in
 	  trace := (depth, None) :: !trace;
-	  raise reraise
+	  iraise reraise
       end
 
 (** For info, from the linear trace information, we reconstitute the part
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 9a241c7ef1..13742f7405 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -71,9 +71,9 @@ let contradiction_context =
 	           filter_hyp (fun typ -> is_conv_leq typ t)
 		     (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
                  end)
-                 begin function
+                 begin function (e, info) -> match e with
 	           | Not_found -> seek_neg rest
-                   | e -> Proofview.tclZERO e
+                   | e -> Proofview.tclZERO ~info e
                  end)
 	  | _ -> seek_neg rest
     in
@@ -108,9 +108,9 @@ let contradiction_term (c,lbind as cl) =
           else
             Proofview.tclZERO Not_found
         end
-        begin function
+        begin function (e, info) -> match e with
           | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
-          | e -> Proofview.tclZERO e
+          | e -> Proofview.tclZERO ~info e
         end
   end
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 303c73d6bb..ca1cc75064 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -228,6 +228,7 @@ module SearchProblem = struct
 (* 	      msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
 	      (lgls,pptac) :: aux tacl
 	  with e when Errors.noncritical e ->
+            let e = Errors.push e in
             Refiner.catch_failerror e; aux tacl
     in aux l
 
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index a43e99a7f2..df8a018bb8 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -157,9 +157,9 @@ let solveEqBranch rectype =
             (tclTHEN (choose_eq eqonleft) intros_reflexivity)
       end
     end
-    begin function
+    begin function (e, info) -> match e with
       | PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!"))
-      | e -> Proofview.tclZERO e
+      | e -> Proofview.tclZERO ~info e
     end
 
 (* The tactic Decide Equality *)
@@ -184,10 +184,10 @@ let decideGralEquality =
              (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
       end
     end
-    begin function
+    begin function (e, info) -> match e with
       | PatternMatchingFailure ->
           Proofview.tclZERO (UserError ("", Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}."))
-      | e -> Proofview.tclZERO e
+      | e -> Proofview.tclZERO ~info e
     end
 
 let decideEqualityGoal = tclTHEN intros decideGralEquality
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 =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 289014a58b..436a66ad26 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -627,7 +627,8 @@ let hResolve id c occ t =
       Pretyping.understand env sigma t_hole
     with
       | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e ->
-          let loc = match Loc.get_loc e with None -> Loc.ghost | Some loc -> loc in
+          let (e, info) = Errors.push e in
+          let loc = match Loc.get_loc info with None -> Loc.ghost | Some loc -> loc in
           resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole)
   in
   let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in
diff --git a/tactics/inv.ml b/tactics/inv.ml
index d0de08c271..39310798d5 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -472,7 +472,7 @@ let raw_inversion inv_kind id status names =
   end
 
 (* Error messages of the inversion tactics *)
-let wrap_inv_error id = function
+let wrap_inv_error id = function (e, info) -> match e with
   | Indrec.RecursionSchemeError
       (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) ->
       Proofview.tclENV >>= fun env ->
@@ -481,7 +481,7 @@ let wrap_inv_error id = function
 	pr_sort k ++
 	strbrk " which is not allowed for inductive definition " ++
 	pr_inductive env (fst i) ++ str "."))
-  | e -> Proofview.tclZERO e
+  | e -> Proofview.tclZERO ~info e
 
 (* The most general inversion tactic *)
 let inversion inv_kind status names id =
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 1245e7c298..9d9847ea57 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -2011,15 +2011,15 @@ let setoid_proof ty fn fallback =
         | e ->
             Proofview.tclORELSE
               fallback
-              begin function
+              begin function (e', info) -> match e' with
                 | Hipattern.NoEquationFound ->
 	            begin match e with
-	            | Not_found ->
+	            | (Not_found, _) ->
 	                let rel, _, _ = decompose_app_rel env sigma concl in
 		        not_declared env ty rel
-	            | _ -> Proofview.tclZERO e
+	            | (e, info) -> Proofview.tclZERO ~info e
                     end
-                | e' -> Proofview.tclZERO e'
+                | e' -> Proofview.tclZERO ~info e'
               end
       end
   end
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index fc31c3a994..dd937cf6a1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -128,15 +128,15 @@ end
 
 let dloc = Loc.ghost
 
-let catching_error call_trace fail e =
+let catching_error call_trace fail (e, info) =
   let inner_trace =
-    Option.default [] (Exninfo.get e ltac_trace_info)
+    Option.default [] (Exninfo.get info ltac_trace_info)
   in
-  if List.is_empty call_trace && List.is_empty inner_trace then fail e
+  if List.is_empty call_trace && List.is_empty inner_trace then fail (e, info)
   else begin
     assert (Errors.noncritical e); (* preserved invariant *)
     let new_trace = inner_trace @ call_trace in
-    let located_exc = Exninfo.add e ltac_trace_info new_trace in
+    let located_exc = (e, Exninfo.add info ltac_trace_info new_trace) in
     fail located_exc
   end
 
@@ -144,12 +144,12 @@ let catch_error call_trace f x =
   try f x
   with e when Errors.noncritical e ->
     let e = Errors.push e in
-    catching_error call_trace raise e
+    catching_error call_trace iraise e
 
 let catch_error_tac call_trace tac =
   Proofview.tclORELSE
     tac
-    (catching_error call_trace Proofview.tclZERO)
+    (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
 
 let curr_debug ist = match TacStore.get ist.extra f_debug with
 | None -> DebugOff
@@ -747,9 +747,9 @@ let interp_may_eval f ist env sigma = function
        (* spiwack: to avoid unnecessary modifications of tacinterp, as this
           function already use effect, I call [run] hoping it doesn't mess
           up with any assumption. *)
-       Proofview.NonLogical.run (debugging_exception_step ist false reraise (fun () ->
+       Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () ->
          str"interpretation of term " ++ pr_glob_constr_env env (fst c)));
-       raise reraise
+       iraise reraise
 
 (* Interprets a constr expression possibly to first evaluate *)
 let interp_constr_may_eval ist env sigma c =
@@ -761,8 +761,8 @@ let interp_constr_may_eval ist env sigma c =
       (* spiwack: to avoid unnecessary modifications of tacinterp, as this
           function already use effect, I call [run] hoping it doesn't mess
           up with any assumption. *)
-       Proofview.NonLogical.run (debugging_exception_step ist false reraise (fun () -> str"evaluation of term"));
-      raise reraise
+       Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> str"evaluation of term"));
+      iraise reraise
   in
   begin
     (* spiwack: to avoid unnecessary modifications of tacinterp, as this
@@ -1462,9 +1462,9 @@ and interp_app loc ist fv largs : typed_generic_argument Ftactic.t =
               catch_error_tac trace (val_interp ist body) >>= fun v ->
               Ftactic.return (name_vfun (push_appl appl largs) v)
             end
-	    begin fun e ->
+	    begin fun (e, info) ->
               Proofview.tclLIFT (debugging_exception_step ist false e (fun () -> str "evaluation")) <*>
-	      Proofview.tclZERO e
+	      Proofview.tclZERO ~info e
             end
         end >>= fun v ->
         (* No errors happened, we propagate the trace *)
@@ -1553,9 +1553,9 @@ and interp_match_successes lz ist tac =
       let tac = Proofview.tclONCE tac in
       tac >>= fun ans -> interp_match_success ist ans
     else
-      let break e = match e with
+      let break (e, info) = match e with
       | FailError (0, _) -> None
-      | FailError (n, s) -> Some (FailError (pred n, s))
+      | FailError (n, s) -> Some (FailError (pred n, s), info)
       | _ -> None
       in
       let tac = Proofview.tclBREAK break tac >>= fun ans -> interp_match_success ist ans in
@@ -1568,10 +1568,10 @@ and interp_match ist lz constr lmr =
   begin Proofview.tclORELSE
     (interp_ltac_constr ist constr)
     begin function
-      | e ->
+      | (e, info) ->
           Proofview.tclLIFT (debugging_exception_step ist true e
           (fun () -> str "evaluation of the matched expression")) <*>
-          Proofview.tclZERO e
+          Proofview.tclZERO ~info e
     end
   end >>= fun constr ->
   Ftactic.enter begin fun gl ->
@@ -1715,7 +1715,7 @@ and interp_ltac_constr ist e : constr Ftactic.t =
   let (>>=) = Ftactic.bind in
   begin Proofview.tclORELSE
       (val_interp ist e)
-      begin function
+      begin function (err, info) -> match err with
         | Not_found ->
             Ftactic.enter begin fun gl ->
               let env = Proofview.Goal.env gl in
@@ -1726,7 +1726,7 @@ and interp_ltac_constr ist e : constr Ftactic.t =
               end
             <*> Proofview.tclZERO Not_found
             end
-        | e -> Proofview.tclZERO e
+        | err -> Proofview.tclZERO ~info err
       end
   end >>= fun result ->
   Ftactic.enter begin fun gl ->
@@ -2348,9 +2348,8 @@ let _ =
         try Proof.run_tactic env tac prf
         with Logic_monad.TacticFailure e as src ->
           (** Catch the inner error of the monad tactic *)
-          let src = Errors.push src in
-          let e = Backtrace.app_backtrace ~src ~dst:e in
-          raise e
+          let (_, info) = Errors.push src in
+          iraise (e, info)
       in
       (** Plug back the retrieved sigma *)
       let sigma = Proof.in_proof prf (fun sigma -> sigma) in
diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml
index c662fad0be..52fa2e4a2d 100644
--- a/tactics/tacticMatching.ml
+++ b/tactics/tacticMatching.ml
@@ -104,6 +104,8 @@ let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) =
 let matching_error =
   Errors.UserError ("tactic matching" , Pp.str "No matching clauses for match.")
 
+let imatching_error = (matching_error, Exninfo.null)
+
 (** A functor is introduced to share the environment and the
     evar_map. They do not change and it would be a pity to introduce
     closures everywhere just for the occasional calls to
@@ -191,12 +193,12 @@ module PatternMatching (E:StaticEnvironment) = struct
     m.stream eval ctx
 
   (** Chooses in a list, in the same order as the list *)
-  let rec pick (l:'a list) e : 'a m = match l with
-  | [] -> { stream = fun _ _ -> Proofview.tclZERO e }
+  let rec pick (l:'a list) (e, info) : 'a m = match l with
+  | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e }
   | x :: l ->
     { stream = fun k ctx -> Proofview.tclOR (k x ctx) (fun e -> (pick l e).stream k ctx) }
 
-  let pick l = pick l matching_error
+  let pick l = pick l imatching_error
 
   (** Declares a subsitution, a context substitution and a term substitution. *)
   let put subst context terms : unit m =
@@ -234,20 +236,20 @@ module PatternMatching (E:StaticEnvironment) = struct
         end
     | Subterm (with_app_context,id_ctxt,p) ->
 
-      let rec map s e =
+      let rec map s (e, info) =
         { stream = fun k ctx -> match IStream.peek s with
-          | IStream.Nil -> Proofview.tclZERO e
+          | IStream.Nil -> Proofview.tclZERO ~info e
           | IStream.Cons ({ ConstrMatching.m_sub ; m_ctx }, s) ->
             let subst = adjust m_sub in
             let context = id_map_try_add id_ctxt m_ctx Id.Map.empty in
             let terms = empty_term_subst in
             let nctx = { subst ; context ; terms ; lhs = () } in
             match merge ctx nctx with
-            | None -> (map s e).stream k ctx
+            | None -> (map s (e, info)).stream k ctx
             | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx)
         }
       in
-      map (ConstrMatching.match_subterm_gen E.env E.sigma with_app_context p term) matching_error
+      map (ConstrMatching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error
 
 
   (** [rule_match_term term rule] matches the term [term] with the
@@ -261,8 +263,8 @@ module PatternMatching (E:StaticEnvironment) = struct
 
   (** [match_term term rules] matches the term [term] with the set of
       matching rules [rules].*)
-  let rec match_term e term rules = match rules with
-  | [] -> { stream = fun _ _ -> Proofview.tclZERO e }
+  let rec match_term (e, info) term rules = match rules with
+  | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e }
   | r :: rules ->
     { stream = fun k ctx ->
       let head = rule_match_term term r in
@@ -333,8 +335,8 @@ module PatternMatching (E:StaticEnvironment) = struct
 
   (** [match_goal hyps concl rules] matches the goal [hyps|-concl]
       with the set of matching rules [rules]. *)
-  let rec match_goal e hyps concl rules = match rules with
-  | [] -> { stream = fun _ _ -> Proofview.tclZERO e }
+  let rec match_goal (e, info) hyps concl rules = match rules with
+  | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e }
   | r :: rules ->
     { stream = fun k ctx ->
       let head = rule_match_goal hyps concl r in
@@ -354,7 +356,7 @@ let match_term env sigma term rules =
     let sigma = sigma
   end in
   let module M = PatternMatching(E) in
-  M.run (M.match_term matching_error term rules)
+  M.run (M.match_term imatching_error term rules)
 
 
 (** [match_goal env sigma hyps concl rules] matches the goal
@@ -368,4 +370,4 @@ let match_goal env sigma hyps concl rules =
     let sigma = sigma
   end in
   let module M = PatternMatching(E) in
-  M.run (M.match_goal matching_error hyps concl rules)
+  M.run (M.match_goal imatching_error hyps concl rules)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 82ec155595..5c899aefc2 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 =
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index fbdc6d94e1..49cae37a7b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -156,7 +156,7 @@ module New : sig
 
   (** [catch_failerror e] fails and decreases the level if [e] is an
       Ltac error with level more than 0. Otherwise succeeds. *)
-  val catch_failerror : exn -> unit tactic
+  val catch_failerror : Util.iexn -> unit tactic
 
   val tclIDTAC : unit tactic
   val tclTHEN : unit tactic -> unit tactic -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 40228c4df5..26fd773232 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -763,11 +763,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
 	  Proofview.tclORELSE
 	  (Tacticals.New.tclTHEN (Proofview.V82.tactic hnf_in_concl)
 	     (intro_then_gen name_flag move_flag false dep_flag tac))
-          begin function
+          begin function (e, info) -> match e with
             | RefinerError IntroNeedsProduct ->
                 Proofview.tclZERO 
 		  (Errors.UserError("Intro",str "No product even after head-reduction."))
-            | e -> Proofview.tclZERO e
+            | e -> Proofview.tclZERO ~info e
           end
   end
 
@@ -805,10 +805,10 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
       intro_then_gen name_flag move_flag false dep_flag
          (fun id -> aux (n+1) (id::ids))
       end
-      begin function
+      begin function (e, info) -> match e with
       | RefinerError IntroNeedsProduct ->
           tac ids
-      | e -> Proofview.tclZERO e
+      | e -> Proofview.tclZERO ~info e
       end
     else
       tac ids
@@ -1246,12 +1246,12 @@ let default_elim with_evars clear_flag (c,_ as cx) =
 	Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd)
 	  (general_elim with_evars clear_flag cx elim)
     end)
-    begin function
+    begin function (e, info) -> match e with
       | IsNonrec ->
           (* For records, induction principles aren't there by default
              anymore.  Instead, we do a case analysis instead. *)
           general_case_analysis with_evars clear_flag cx
-      | e -> Proofview.tclZERO e
+      | e -> Proofview.tclZERO ~info e
     end
 
 let elim_in_context with_evars clear_flag c = function
@@ -1452,16 +1452,18 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
     in
     Proofview.tclORELSE
       (try_apply thm_ty0 concl_nprod)
-      (function PretypeError _|RefinerError _|UserError _|Failure _ as exn0 ->
+      (function (e, info) -> match e with
+        | PretypeError _|RefinerError _|UserError _|Failure _ as exn0 ->
 	let rec try_red_apply thm_ty =
           try 
             (* Try to head-reduce the conclusion of the theorem *)
             let red_thm = try_red_product env sigma thm_ty in
             Proofview.tclORELSE
               (try_apply red_thm concl_nprod)
-              (function PretypeError _|RefinerError _|UserError _|Failure _ ->
+              (function (e, info) -> match e with
+              | PretypeError _|RefinerError _|UserError _|Failure _ ->
 		try_red_apply red_thm
-              | exn -> raise exn)
+              | exn -> iraise (exn, info))
           with Redelimination ->
             (* Last chance: if the head is a variable, apply may try
 	       second order unification *)
@@ -1472,22 +1474,26 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
                     Tacticals.New.tclTHEN
                       (try_main_apply b (mkVar id))
                       (Proofview.V82.tactic (thin [id])))
-                  (fun _ -> Proofview.tclZERO (Loc.add_loc exn0 loc)) c
+                  (fun _ ->
+                    let info = Loc.add_loc info loc in
+                    Proofview.tclZERO ~info exn0) c
 	      else
-		Proofview.tclZERO (Loc.add_loc exn0 loc) in
+                let info = Loc.add_loc info loc in
+		Proofview.tclZERO ~info exn0 in
             if not (Int.equal concl_nprod 0) then
               try
                 Proofview.tclORELSE
                   (try_apply thm_ty 0)
-                  (function PretypeError _|RefinerError _|UserError _|Failure _->
+                  (function (e, info) -> match e with
+                  | PretypeError _|RefinerError _|UserError _|Failure _->
                     tac
-                  | exn -> raise exn)
+                  | exn -> iraise (exn, info))
               with UserError _ | Exit ->
                 tac
             else
               tac
 	in try_red_apply thm_ty0
-      | exn -> raise exn)
+      | exn -> iraise (exn, info))
     end
   in
     Tacticals.New.tclTHENLIST [
@@ -1570,7 +1576,7 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) =
     with e when Errors.noncritical e ->
     let e = Errors.push e in
     try aux (clenv_push_prod clause)
-    with NotExtensibleClause -> raise e
+    with NotExtensibleClause -> iraise e
   in
   aux (make_clenv_binding env sigma (d,thm) lbind)
 
@@ -1601,7 +1607,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
       let e = Errors.push e in
         (descend_in_conjunctions [targetid]
            (fun b id -> aux (id::idstoclear) b (mkVar id))
-           (fun _ -> raise e) c)
+           (fun _ -> iraise e) c)
     end
   in
   aux [] with_destruct d
@@ -2652,14 +2658,14 @@ let dest_intro_patterns avoid thin dest pat tac =
 let safe_dest_intro_patterns avoid thin dest pat tac =
   Proofview.tclORELSE
     (dest_intro_patterns avoid thin dest pat tac)
-    begin function
+    begin function (e, info) -> match e with
       | UserError ("move_hyp",_) ->
        (* May happen e.g. with "destruct x using s" with an hypothesis
           which is morally an induction hypothesis to be "MoveLast" if
           known as such but which is considered instead as a subterm of
           a constructor to be move at the place of x. *)
           dest_intro_patterns avoid thin MoveLast pat tac
-      | e -> Proofview.tclZERO e
+      | e -> Proofview.tclZERO ~info e
     end
 
 type elim_arg_kind = RecArg | IndArg | OtherArg
@@ -4155,9 +4161,9 @@ let reflexivity_red allowred =
 let reflexivity =
   Proofview.tclORELSE
     (reflexivity_red false)
-    begin function
+    begin function (e, info) -> match e with
       | NoEquationFound -> Hook.get forward_setoid_reflexivity
-      | e -> Proofview.tclZERO e
+      | e -> Proofview.tclZERO ~info e
     end
 
 let intros_reflexivity  = (Tacticals.New.tclTHEN intros reflexivity)
@@ -4209,9 +4215,9 @@ let symmetry_red allowred =
 let symmetry =
   Proofview.tclORELSE
     (symmetry_red false)
-    begin function
+    begin function (e, info) -> match e with
       | NoEquationFound -> Hook.get forward_setoid_symmetry
-      | e -> Proofview.tclZERO e
+      | e -> Proofview.tclZERO ~info e
     end
 
 let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
@@ -4232,9 +4238,9 @@ let symmetry_in id =
           [ intro_replacing id;
             Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
     end
-    begin function
+    begin function (e, info) -> match e with
       | NoEquationFound -> Hook.get forward_setoid_symmetry_in id
-      | e -> Proofview.tclZERO e
+      | e -> Proofview.tclZERO ~info e
     end
   end
 
@@ -4306,9 +4312,9 @@ let transitivity_red allowred t =
 let transitivity_gen t =
   Proofview.tclORELSE
     (transitivity_red false t)
-    begin function
+    begin function (e, info) -> match e with
       | NoEquationFound -> Hook.get forward_setoid_transitivity t
-      | e -> Proofview.tclZERO e
+      | e -> Proofview.tclZERO ~info e
     end
 
 let etransitivity = transitivity_gen None
@@ -4365,9 +4371,8 @@ let abstract_subproof id gk tac =
        which is an error irrelevant to the proof system (in fact it
        means that [e] comes from [tac] failing to yield enough
        success). Hence it reraises [e]. *)
-    let src = Errors.push src in
-    let e = Backtrace.app_backtrace ~src ~dst:e in
-    raise e
+    let (_, info) = Errors.push src in
+    iraise (e, info)
   in
   let cd = Entries.DefinitionEntry const in
   let decl = (cd, IsProof Lemma) in
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 346f560f8d..075f66751f 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -314,10 +314,10 @@ let intuition_gen ist flags tac =
 let tauto_intuitionistic flags =
   Proofview.tclORELSE
     (intuition_gen (default_ist ()) flags <:tactic<fail>>)
-    begin function
+    begin function (e, info) -> match e with
       | Refiner.FailError _ | UserError _ ->
           Proofview.tclZERO (UserError ("tauto" , str "tauto failed."))
-      | e -> Proofview.tclZERO e
+      | e -> Proofview.tclZERO ~info e
     end
 
 let coq_nnpp_path =
@@ -327,9 +327,9 @@ let coq_nnpp_path =
 let tauto_classical flags nnpp =
   Proofview.tclORELSE
     (Tacticals.New.tclTHEN (apply nnpp) (tauto_intuitionistic flags))
-    begin function
+    begin function (e, info) -> match e with
       | UserError _ -> Proofview.tclZERO (UserError ("tauto" , str "Classical tauto failed."))
-      | e -> Proofview.tclZERO e
+      | e -> Proofview.tclZERO ~info e
     end
 
 let tauto_gen flags =