Merge PR #11755: [exn] [tactics] improve backtraces on monadic errors

Ack-by: gares
Ack-by: ppedrot

26 files changed, 313 insertions, 144 deletions

diff --git a/clib/exninfo.ml b/clib/exninfo.ml
index 621f7e615f..07b7f47529 100644
--- a/clib/exninfo.ml
+++ b/clib/exninfo.ml
@@ -117,3 +117,10 @@ let capture e =
     e, add info backtrace_info bt
   else
     e, info e
+
+let reify () =
+  if !is_recording then
+    let bt = Printexc.get_callstack 50 in
+    add null backtrace_info bt
+  else
+    null
diff --git a/clib/exninfo.mli b/clib/exninfo.mli
index 55f0662431..08395f59f4 100644
--- a/clib/exninfo.mli
+++ b/clib/exninfo.mli
@@ -79,3 +79,5 @@ val capture : exn -> iexn
 
 val iraise : iexn -> 'a
 (** Raise the given enriched exception. *)
+
+val reify : unit -> info
diff --git a/doc/changelog/12-misc/11755-exn+tclfail.rst b/doc/changelog/12-misc/11755-exn+tclfail.rst
new file mode 100644
index 0000000000..800cc09e01
--- /dev/null
+++ b/doc/changelog/12-misc/11755-exn+tclfail.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Backtrace information for tactics has been improved
+  (`#11755 <https://github.com/coq/coq/pull/11755>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 2e036be9e3..de38104ecd 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -261,13 +261,9 @@ module Monad = Proof
 
 
 (** [tclZERO e] fails with exception [e]. It has no success. *)
-let tclZERO ?info e =
+let tclZERO ?(info=Exninfo.null) e =
   if not (CErrors.noncritical e) then
     CErrors.anomaly (Pp.str "tclZERO receiving critical error: " ++ CErrors.print e);
-  let info = match info with
-  | None -> Exninfo.null
-  | Some info -> info
-  in
   Proof.zero (e, info)
 
 (** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever
@@ -323,9 +319,10 @@ let tclEXACTLY_ONCE e t =
   split t >>= function
     | Nil (e, info) -> tclZERO ~info e
     | Cons (x,k) ->
-        Proof.split (k (e, Exninfo.null)) >>= function
-          | Nil _ -> tclUNIT x
-          | _ -> tclZERO MoreThanOneSuccess
+      let info = Exninfo.null in
+      Proof.split (k (e, Exninfo.null)) >>= function
+      | Nil _ -> tclUNIT x
+      | _ -> tclZERO ~info MoreThanOneSuccess
 
 
 (** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *)
@@ -359,7 +356,7 @@ end
     is restored at the end of the tactic). If the range [i]-[j] is not
     valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *)
 let tclFOCUS ?nosuchgoal i j t =
-  let nosuchgoal = Option.default (tclZERO (NoSuchGoals (j+1-i))) nosuchgoal in
+  let nosuchgoal ~info = Option.default (tclZERO ~info (NoSuchGoals (j+1-i))) nosuchgoal in
   let open Proof in
   Pv.get >>= fun initial ->
   try
@@ -368,7 +365,9 @@ let tclFOCUS ?nosuchgoal i j t =
     t >>= fun result ->
     Pv.modify (fun next -> unfocus context next) >>
     return result
-  with CList.IndexOutOfRange -> nosuchgoal
+  with CList.IndexOutOfRange as exn ->
+    let _, info = Exninfo.capture exn in
+    nosuchgoal ~info
 
 let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t
 
@@ -907,7 +906,8 @@ let tclPROGRESS t =
   if not test then
     tclUNIT res
   else
-    tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
+    let info = Exninfo.reify () in
+    tclZERO ~info (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
 
 let _ = CErrors.register_handler begin function
   | Logic_monad.Tac_Timeout ->
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 81e745b714..35c90444b1 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -142,7 +142,9 @@ let progress_evars t =
         let sigma = Tacmach.New.project gl' in
         let newconcl = Proofview.Goal.concl gl' in
         if eq_constr_mod_evars sigma concl newconcl
-        then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)")
+        then
+          let info = Exninfo.reify () in
+          Tacticals.New.tclFAIL ~info 0 (Pp.str"No progress made (modulo evars)")
         else Proofview.tclUNIT ()
       end
     in t <*> check
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index d6b2a17882..4bc8d61258 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1566,7 +1566,8 @@ let assert_replacing id newt tac =
   Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
 
 let newfail n s =
-  Proofview.tclZERO (Refiner.FailError (n, lazy s))
+  let info = Exninfo.reify () in
+  Proofview.tclZERO ~info (Refiner.FailError (n, lazy s))
 
 let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let open Proofview.Notations in
@@ -1576,8 +1577,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let treat sigma res =
     match res with
     | None -> newfail 0 (str "Nothing to rewrite")
-    | Some None -> if progress then newfail 0 (str"Failed to progress")
-                   else Proofview.tclUNIT ()
+    | Some None ->
+      if progress
+      then newfail 0 (str"Failed to progress")
+      else Proofview.tclUNIT ()
     | Some (Some res) ->
         let (undef, prf, newt) = res in
         let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
@@ -1641,7 +1644,9 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
 
 let tactic_init_setoid () =
   try init_setoid (); Proofview.tclUNIT ()
-  with e when CErrors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Setoid library not loaded")
+  with e when CErrors.noncritical e ->
+    let _, info = Exninfo.capture e in
+    Tacticals.New.tclFAIL ~info 0 (str"Setoid library not loaded")
 
 let cl_rewrite_clause_strat progress strat clause =
   tactic_init_setoid () <*>
@@ -1650,10 +1655,11 @@ let cl_rewrite_clause_strat progress strat clause =
       (cl_rewrite_clause_newtac ~progress strat clause)
       (fun (e, info) -> match e with
        | RewriteFailure e ->
-         tclZEROMSG (str"setoid rewrite failed: " ++ e)
+         tclZEROMSG ~info (str"setoid rewrite failed: " ++ e)
        | Refiner.FailError (n, pp) ->
-          tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp)
-       | e -> Proofview.tclZERO ~info e))
+         tclFAIL ~info n (str"setoid rewrite failed: " ++ Lazy.force pp)
+       | e ->
+         Proofview.tclZERO ~info e))
 
 (** Setoid rewriting when called with "setoid_rewrite" *)
 let cl_rewrite_clause l left2right occs clause =
@@ -2109,7 +2115,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals =
             (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl)))
     (fun (e, info) -> match e with
     | RewriteFailure e ->
-      tclFAIL 0 (str"setoid rewrite failed: " ++ e)
+      tclFAIL ~info 0 (str"setoid rewrite failed: " ++ e)
     | e -> Proofview.tclZERO ~info e)
   end
 
@@ -2117,8 +2123,8 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite
 
 (** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
 
-let not_declared env sigma ty rel =
-  tclFAIL 0
+let not_declared ~info env sigma ty rel =
+  tclFAIL ~info 0
     (str" The relation " ++ Printer.pr_econstr_env env sigma rel ++ str" is not a declared " ++
      str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library")
 
@@ -2135,7 +2141,10 @@ let setoid_proof ty fn fallback =
           let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in
             (try init_relation_classes () with _ -> raise Not_found);
             fn env sigma car rel
-        with e -> Proofview.tclZERO e
+        with e ->
+          (* XXX what is the right test here as to whether e can be converted ? *)
+          let e, info = Exninfo.capture e in
+          Proofview.tclZERO ~info e
       end
       begin function
         | e ->
@@ -2145,9 +2154,10 @@ let setoid_proof ty fn fallback =
                 | Hipattern.NoEquationFound ->
                     begin match e with
                     | (Not_found, _) ->
-                        let rel, _, _ = decompose_app_rel env sigma concl in
-                        not_declared env sigma ty rel
-                    | (e, info) -> Proofview.tclZERO ~info e
+                      let rel, _, _ = decompose_app_rel env sigma concl in
+                      not_declared ~info env sigma ty rel
+                    | (e, info) ->
+                      Proofview.tclZERO ~info e
                     end
                 | e' -> Proofview.tclZERO ~info e'
               end
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6d350ade8d..5abe18e00c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -774,7 +774,9 @@ let interp_message_token ist = function
   | MsgIdent {loc;v=id} ->
     let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in
     match v with
-    | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (Id.print id ++ str" not found."))
+    | None -> Ftactic.lift (
+        let info = Exninfo.reify () in
+        Tacticals.New.tclZEROMSG ~info (Id.print id ++ str" not found."))
     | Some v -> message_of_value v
 
 let interp_message ist l =
@@ -1087,11 +1089,15 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       end
   | TacFail (g,n,s) ->
       let msg = interp_message ist s in
-      let tac l = Tacticals.New.tclFAIL (interp_int_or_var ist n) l in
+      let tac ~info l = Tacticals.New.tclFAIL ~info (interp_int_or_var ist n) l in
       let tac =
         match g with
-        | TacLocal -> fun l -> Proofview.tclINDEPENDENT (tac l)
-        | TacGlobal -> tac
+        | TacLocal ->
+          let info = Exninfo.reify () in
+          fun l -> Proofview.tclINDEPENDENT (tac ~info l)
+        | TacGlobal ->
+          let info = Exninfo.reify () in
+          tac ~info
       in
       Ftactic.run msg tac
   | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac)
@@ -1174,8 +1180,11 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
         let len1 = List.length alias.Tacenv.alias_args in
         let len2 = List.length l in
         if len1 = len2 then tac
-        else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \
-          expected " ++ int len1 ++ str ", found " ++ int len2)
+        else
+          let info = Exninfo.reify () in
+          Tacticals.New.tclZEROMSG ~info
+            (str "Arguments length mismatch: \
+                  expected " ++ int len1 ++ str ", found " ++ int len2)
       in
       Ftactic.run tac (fun () -> Proofview.tclUNIT ())
 
@@ -1267,7 +1276,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
 and interp_app loc ist fv largs : Val.t Ftactic.t =
   Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
   let (>>=) = Ftactic.bind in
-  let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in
+  let fail ~info = Tacticals.New.tclZEROMSG ~info (str "Illegal tactic application.") in
   if has_type fv (topwit wit_tacvalue) then
   match to_tacvalue fv with
      (* if var=[] and body has been delayed by val_interp, then body
@@ -1313,12 +1322,18 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
         Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body)))
     | (VFun(appl,trace,olfun,[],body)) ->
       let extra_args = List.length largs in
-      Tacticals.New.tclZEROMSG (str "Illegal tactic application: got " ++
-                                str (string_of_int extra_args) ++
-                                str " extra " ++ str (String.plural extra_args "argument") ++
-                                str ".")
-    | VRec(_,_) -> fail
-  else fail
+      let info = Exninfo.reify () in
+      Tacticals.New.tclZEROMSG ~info
+        (str "Illegal tactic application: got " ++
+         str (string_of_int extra_args) ++
+         str " extra " ++ str (String.plural extra_args "argument") ++
+         str ".")
+    | VRec(_,_) ->
+      let info = Exninfo.reify () in
+      fail ~info
+  else
+    let info = Exninfo.reify () in
+    fail ~info
 
 (* Gives the tactic corresponding to the tactic value *)
 and tactic_of_value ist vle =
@@ -1346,7 +1361,8 @@ and tactic_of_value ist vle =
      let givenargs =
        List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in
      let numgiven = List.length givenargs in
-     Tacticals.New.tclZEROMSG
+     let info = Exninfo.reify () in
+     Tacticals.New.tclZEROMSG ~info
        (Pp.str tactic_nm ++ Pp.str " was not fully applied:" ++ spc() ++
           (match numargs with
             0 -> assert false
@@ -1364,11 +1380,15 @@ and tactic_of_value ist vle =
           | _ ->
              Pp.str "arguments were provided for variables " ++
                pr_enum Pp.str givenargs ++ Pp.str ".")
-  | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
+  | VRec _ ->
+    let info = Exninfo.reify () in
+    Tacticals.New.tclZEROMSG ~info (str "A fully applied tactic is expected.")
   else if has_type vle (topwit wit_tactic) then
     let tac = out_gen (topwit wit_tactic) vle in
     tactic_of_value ist tac
-  else Tacticals.New.tclZEROMSG (str "Expression does not evaluate to a tactic.")
+  else
+    let info = Exninfo.reify () in
+    Tacticals.New.tclZEROMSG ~info (str "Expression does not evaluate to a tactic.")
 
 (* Interprets the clauses of a recursive LetIn *)
 and interp_letrec ist llc u =
@@ -1562,10 +1582,12 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t =
           pr_econstr_env env sigma cresult)
     end <*>
     Ftactic.return cresult
-  with CannotCoerceTo _ ->
+  with CannotCoerceTo _ as exn ->
+    let _, info = Exninfo.capture exn in
     let env = Proofview.Goal.env gl in
-    Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++
-      str "offending expression: " ++ fnl() ++ pr_inspect env e result)
+    Tacticals.New.tclZEROMSG ~info
+      (str "Must evaluate to a closed term" ++ fnl() ++
+       str "offending expression: " ++ fnl() ++ pr_inspect env e result)
   end
 
 
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 525199735d..2b43b11fe1 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -186,7 +186,9 @@ module PatternMatching (E:StaticEnvironment) = struct
     { stream = fun k ctx -> m.stream (fun () ctx -> y.stream k ctx) ctx }
 
   (** Failure of the pattern-matching monad: no success. *)
-  let fail (type a) : a m = { stream = fun _ _ -> Proofview.tclZERO matching_error }
+  let fail (type a) : a m = { stream = fun _ _ ->
+      let info = Exninfo.reify () in
+      Proofview.tclZERO ~info matching_error }
 
   let run (m : 'a m) =
     let ctx = {
@@ -209,7 +211,11 @@ module PatternMatching (E:StaticEnvironment) = struct
   (** Declares a substitution, a context substitution and a term substitution. *)
   let put subst context terms : unit m =
     let s = { subst ; context ; terms ; lhs = () } in
-    { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s }
+    { stream = fun k ctx -> match merge s ctx with
+          | None ->
+            let info = Exninfo.reify () in
+            Proofview.tclZERO ~info matching_error
+          | Some s -> k () s }
 
   (** Declares a substitution. *)
   let put_subst subst : unit m = put subst empty_context_subst empty_term_subst
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 79d6c05e1d..3ba6365783 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1475,7 +1475,9 @@ let coq_omega =
       let path = simplify_strong (new_id,new_var_num,display_var) system in
       if !display_action_flag then display_action display_var path;
       tclTHEN prelude (replay_history tactic_normalisation path)
-    with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system")
+    with NO_CONTRADICTION as e ->
+      let _, info = Exninfo.capture e in
+      tclZEROMSG ~info (Pp.str"Omega can't solve this system")
   end
   end
 
@@ -1890,7 +1892,9 @@ let destructure_goal =
                                          end)
                 intro
             with Undecidable -> Tactics.elim_type (Lazy.force coq_False)
-            | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+            | e when Proofview.V82.catchable_exception e ->
+              let e, info = Exninfo.capture e in
+              Proofview.tclZERO ~info e
           in
           tclTHEN goal_tac destructure_hyps
     in
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 88a3e85211..ad0a31622c 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -194,9 +194,11 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
       Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term));
     tclUNIT (env,sigma,term)
   with e ->
+    (* XXX this is another catch all! *)
+    let e, info = Exninfo.capture e in
     Ssrprinters.ppdebug (lazy
     Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob));
-     tclZERO e
+    tclZERO ~info e
 end
 
 (* Commits the term to the monad *)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 0257a6f204..007d53f911 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -129,5 +129,7 @@ let unify ?(flags=fail_quick_unif_flags) m =
     try
       let evd' = w_unify env evd CONV ~flags m n in
         Proofview.Unsafe.tclEVARSADVANCE evd'
-    with e when CErrors.noncritical e -> Proofview.tclZERO e
+    with e when CErrors.noncritical e ->
+      let info = Exninfo.reify () in
+      Proofview.tclZERO ~info e
   end
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 75aca7e7ff..175c487958 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -525,7 +525,10 @@ let solve ?with_end_tac gi info_lvl tac pr =
       | None -> tac
       | Some _ -> Proofview.Trace.record_info_trace tac
     in
-    let nosuchgoal = Proofview.tclZERO (SuggestNoSuchGoals (1,pr)) in
+    let nosuchgoal =
+      let info = Exninfo.reify () in
+      Proofview.tclZERO ~info (SuggestNoSuchGoals (1,pr))
+    in
     let tac = let open Goal_select in match gi with
       | SelectAlreadyFocused ->
         let open Proofview.Notations in
@@ -537,7 +540,8 @@ let solve ?with_end_tac gi info_lvl tac pr =
                Pp.(str "Expected a single focused goal but " ++
                    int n ++ str " goals are focused."))
           in
-          Proofview.tclZERO e
+          let info = Exninfo.reify () in
+          Proofview.tclZERO ~info e
 
       | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
       | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 0bf0cd7b63..a10bbcbdd4 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -132,4 +132,7 @@ let solve_constraints =
   tclENV >>= fun env -> tclEVARMAP >>= fun sigma ->
    try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
        Unsafe.tclEVARSADVANCE sigma
-   with e -> tclZERO e
+   with e ->
+     (* XXX this is absorbing anomalies? *)
+     let info = Exninfo.reify () in
+     tclZERO ~info e
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 5b06088518..681c4e910f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -137,8 +137,9 @@ let conclPattern concl pat tac =
     | Some pat ->
         try
           Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
-        with Constr_matching.PatternMatchingFailure ->
-          Tacticals.New.tclZEROMSG (str "pattern-matching failed")
+        with Constr_matching.PatternMatchingFailure as exn ->
+          let _, info = Exninfo.capture exn in
+          Tacticals.New.tclZEROMSG ~info (str "pattern-matching failed")
   in
   Proofview.Goal.enter begin fun gl ->
      let env = Proofview.Goal.env gl in
@@ -383,7 +384,9 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
 and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
   let tactic = function
     | Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl)
-    | ERes_pf _ -> Proofview.Goal.enter (fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf"))
+    | ERes_pf _ -> Proofview.Goal.enter (fun gl ->
+        let info = Exninfo.reify () in
+        Tacticals.New.tclZEROMSG ~info (str "eres_pf"))
     | Give_exact (c, cl)  -> exact poly (c, cl)
     | Res_pf_THEN_trivial_fail (c,cl) ->
       Tacticals.New.tclTHEN
@@ -395,7 +398,9 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
       Proofview.Goal.enter begin fun gl ->
        if exists_evaluable_reference (Tacmach.New.pf_env gl) c then
          Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
-       else Tacticals.New.tclFAIL 0 (str"Unbound reference")
+       else
+         let info = Exninfo.reify () in
+         Tacticals.New.tclFAIL ~info 0 (str"Unbound reference")
        end
     | Extern tacast ->
       conclPattern concl p tacast
@@ -492,7 +497,10 @@ let search d n mod_delta db_list local_db =
     (* spiwack: the test of [n] to 0 must be done independently in
        each goal. Hence the [tclEXTEND] *)
     Proofview.tclEXTEND [] begin
-      if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else
+      if Int.equal n 0 then
+        let info = Exninfo.reify () in
+        Tacticals.New.tclZEROMSG ~info (str"BOUND 2")
+      else
         Tacticals.New.tclORELSE0 (dbg_assumption d)
           (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
              ( Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index ac83acd726..eaefa2947a 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -154,7 +154,8 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
   if not (Locusops.is_all_occurrences cl.concl_occs) &&
      cl.concl_occs != NoOccurrences
   then
-    Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.")
+    let info = Exninfo.reify () in
+    Tacticals.New.tclZEROMSG ~info (str"The \"at\" syntax isn't available yet for the autorewrite tactic.")
   else
     let compose_tac t1 t2 =
       match cl.onhyps with
@@ -185,7 +186,9 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl =
         *)
         Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds tac_main lbas cl)
     | _ ->
-        Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
+      let info = Exninfo.reify () in
+      Tacticals.New.tclZEROMSG ~info
+        (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
 
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a51fc8b347..80c76bee60 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -166,7 +166,9 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
   Proofview.Goal.enter begin fun gls ->
     let resolve =
       try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls)
-      with e when noncritical e -> Proofview.tclZERO e
+      with e when noncritical e ->
+        let _, info = Exninfo.capture e in
+        Proofview.tclZERO ~info e
     in resolve >>= fun clenv' ->
        Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
   end
@@ -207,12 +209,14 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
 let unify_resolve_refine poly flags gl clenv =
   Proofview.tclORELSE
     (unify_resolve_refine poly flags gl clenv)
-    (fun ie ->
-      match fst ie with
+    (fun (exn,info) ->
+      match exn with
       | Evarconv.UnableToUnify _ ->
-         Tacticals.New.tclZEROMSG (str "Unable to unify")
-      | e ->
-         Tacticals.New.tclZEROMSG (str "Unexpected error"))
+        Tacticals.New.tclZEROMSG ~info (str "Unable to unify")
+      | e when CErrors.noncritical e ->
+        Tacticals.New.tclZEROMSG ~info (str "Unexpected error")
+      | _ ->
+        Exninfo.iraise (exn,info))
 
 (** Dealing with goals of the form A -> B and hints of the form
   C -> A -> B.
@@ -234,10 +238,13 @@ let with_prods nprods poly (c, clenv) f =
   if get_typeclasses_limit_intros () then
     Proofview.Goal.enter begin fun gl ->
       try match clenv_of_prods poly nprods (c, clenv) gl with
-          | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
+          | None ->
+            let info = Exninfo.reify () in
+            Tacticals.New.tclZEROMSG ~info (str"Not enough premisses")
           | Some (diff, clenv') -> f gl (c, diff, clenv')
       with e when CErrors.noncritical e ->
-        Tacticals.New.tclZEROMSG (CErrors.print e) end
+        let e, info = Exninfo.capture e in
+        Tacticals.New.tclZEROMSG ~info (CErrors.print e) end
   else Proofview.Goal.enter
          begin fun gl ->
          if Int.equal nprods 0 then f gl (c, None, clenv)
@@ -811,7 +818,9 @@ module Search = struct
       search_tac hints limit (succ depth) info
     in
     fun info ->
-    if Int.equal depth (succ limit) then Proofview.tclZERO ReachedLimitEx
+    if Int.equal depth (succ limit) then
+      let info = Exninfo.reify () in
+      Proofview.tclZERO ~info ReachedLimitEx
     else
       Proofview.tclOR (hints_tac hints info kont)
                       (fun e -> Proofview.tclOR (intro info kont)
@@ -860,9 +869,13 @@ module Search = struct
   let fix_iterative_limit limit t =
     let open Proofview in
     let rec aux depth =
-      if Int.equal depth (succ limit) then tclZERO ReachedLimitEx
-      else tclOR (t depth) (function (ReachedLimitEx, _) -> aux (succ depth)
-                                   | (e,ie) -> Proofview.tclZERO ~info:ie e)
+      if Int.equal depth (succ limit)
+      then
+        let info = Exninfo.reify () in
+        tclZERO ~info ReachedLimitEx
+      else tclOR (t depth) (function
+          | (ReachedLimitEx, _) -> aux (succ depth)
+          | (e,ie) -> Proofview.tclZERO ~info:ie e)
     in aux 1
 
   let eauto_tac_stuck mst ?(unique=false)
@@ -884,18 +897,18 @@ module Search = struct
         | None -> fix_iterative search
         | Some l -> fix_iterative_limit l search
     in
-    let error (e, ie) =
+    let error (e, info) =
       match e with
       | ReachedLimitEx ->
-         Tacticals.New.tclFAIL 0 (str"Proof search reached its limit")
+        Tacticals.New.tclFAIL ~info 0 (str"Proof search reached its limit")
       | NoApplicableEx ->
-         Tacticals.New.tclFAIL 0 (str"Proof search failed" ++
+        Tacticals.New.tclFAIL ~info 0 (str"Proof search failed" ++
                                     (if Option.is_empty depth then mt()
                                      else str" without reaching its limit"))
       | Proofview.MoreThanOneSuccess ->
-         Tacticals.New.tclFAIL 0 (str"Proof search failed: " ++
-                                  str"more than one success found")
-      | e -> Proofview.tclZERO ~info:ie e
+        Tacticals.New.tclFAIL ~info 0 (str"Proof search failed: " ++
+                                       str"more than one success found")
+      | e -> Proofview.tclZERO ~info e
     in
     let tac = Proofview.tclOR tac error in
     let tac =
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index d6be714dd9..8ad3d072ec 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -49,7 +49,9 @@ let absurd c = absurd c
 (** [f] does not assume its argument to be [nf_evar]-ed. *)
 let filter_hyp f tac =
   let rec seek = function
-    | [] -> Proofview.tclZERO Not_found
+    | [] ->
+      let info = Exninfo.reify () in
+      Proofview.tclZERO ~info Not_found
     | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d)
     | _::rest -> seek rest in
   Proofview.Goal.enter begin fun gl ->
@@ -62,7 +64,9 @@ let contradiction_context =
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     let rec seek_neg l = match l with
-      | [] ->  Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
+      | [] ->
+        let info = Exninfo.reify () in
+        Tacticals.New.tclZEROMSG ~info (Pp.str"No such contradiction")
       | d :: rest ->
           let id = NamedDecl.get_id d in
           let typ = nf_evar sigma (NamedDecl.get_type d) in
@@ -83,7 +87,8 @@ let contradiction_context =
                    (* Checking on the fly that it type-checks *)
                    simplest_elim (mkApp (mkVar id,[|p|]))
                | None ->
-                 Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type."))
+                 let info = Exninfo.reify () in
+                 Tacticals.New.tclZEROMSG ~info (Pp.str"Not a negated unit type."))
               (Proofview.tclORELSE
                  (Proofview.Goal.enter begin fun gl ->
                    let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
@@ -123,10 +128,12 @@ let contradiction_term (c,lbind as cl) =
             filter_hyp (fun c -> is_negation_of env sigma typ c)
               (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
           else
-            Proofview.tclZERO Not_found
+            let info = Exninfo.reify () in
+            Proofview.tclZERO ~info Not_found
         end
         begin function (e, info) -> match e with
-          | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.")
+          | Not_found ->
+            Tacticals.New.tclZEROMSG ~info (Pp.str"Not a contradiction.")
           | e -> Proofview.tclZERO ~info e
         end
   end
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 7b323ee0ed..710e0a6808 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -526,5 +526,7 @@ let autounfold_one db cl =
       match cl with
       | Some hyp -> change_in_hyp ~check:true None (make_change_arg c') hyp
       | None -> convert_concl ~check:false c' DEFAULTcast
-    else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
+    else
+      let info = Exninfo.reify () in
+      Tacticals.New.tclFAIL ~info 0 (str "Nothing to unfold")
   end
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 5d8698916f..415c980c2a 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -160,7 +160,8 @@ let double_ind h1 h2 =
   let abs =
     if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else
     if abs_i > abs_j then  Proofview.tclUNIT (abs_j,abs_i) else
-      tclZEROMSG (Pp.str "Both hypotheses are the same.") in
+      let info = Exninfo.reify () in
+      tclZEROMSG ~info (Pp.str "Both hypotheses are the same.") in
   abs >>= fun (abs_i,abs_j) ->
   (tclTHEN (tclDO abs_i intro)
      (onLastHypId
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 6fbd29def9..57d793b2a5 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -182,7 +182,9 @@ let match_eqdec env sigma c =
       let neq = mkApp (noteq,[|mkApp (eq2,[|t;x;y|])|]) in
       if eqonleft then mkApp (op,[|eq;neq|]) else mkApp (op,[|neq;eq|]) in
     Proofview.tclUNIT (eqonleft,mk,c1,c2,ty)
-  with PatternMatchingFailure -> Proofview.tclZERO PatternMatchingFailure
+  with PatternMatchingFailure as exn ->
+    let _, info = Exninfo.capture exn in
+    Proofview.tclZERO ~info PatternMatchingFailure
 
 (* /spiwack *)
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 58345ac253..79b6dfe920 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -280,8 +280,9 @@ let general_elim_clause with_evars frzevars cls rew elim =
     end
     begin function (e, info) -> match e with
     | PretypeError (env, evd, NoOccurrenceFound (c', _)) ->
-      Proofview.tclZERO (PretypeError (env, evd, NoOccurrenceFound (c', cls)))
-    | e -> Proofview.tclZERO ~info e
+      Proofview.tclZERO ~info (PretypeError (env, evd, NoOccurrenceFound (c', cls)))
+    | e ->
+      Proofview.tclZERO ~info e
     end
 
 let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
@@ -1036,7 +1037,9 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
       Proofview.tclUNIT
         (build_discriminator e_env sigma true_0 (false_0,false_ty) dirn (mkVar e) cpath)
     with
-      UserError _ as ex -> Proofview.tclZERO ex
+      UserError _ as ex ->
+      let _, info = Exninfo.capture ex in
+      Proofview.tclZERO ~info ex
   in
     discriminator >>= fun discriminator ->
     discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf ->
@@ -1052,9 +1055,10 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
     let env = Proofview.Goal.env gl in
     match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with
     | Inr _ ->
-        tclZEROMSG (str"Not a discriminable equality.")
+      let info = Exninfo.reify () in
+      tclZEROMSG ~info (str"Not a discriminable equality.")
     | Inl (cpath, (_,dirn), _) ->
-        discr_positions env sigma u eq_clause cpath dirn
+      discr_positions env sigma u eq_clause cpath dirn
   end
 
 let onEquality with_evars tac (c,lbindc) =
@@ -1083,7 +1087,8 @@ let onNegatedEquality with_evars tac =
           (onLastHypId (fun id ->
             onEquality with_evars tac (mkVar id,NoBindings)))
     | _ ->
-        tclZEROMSG (str "Not a negated primitive equality.")
+      let info = Exninfo.reify () in
+      tclZEROMSG ~info (str "Not a negated primitive equality.")
   end
 
 let discrSimpleClause with_evars = function
@@ -1625,10 +1630,11 @@ let cutSubstInHyp l2r eqn id =
 let try_rewrite tac =
   Proofview.tclORELSE tac begin function (e, info) -> match e with
     | Constr_matching.PatternMatchingFailure ->
-        tclZEROMSG (str "Not a primitive equality here.")
+      tclZEROMSG ~info (str "Not a primitive equality here.")
     | e ->
-        tclZEROMSG
-          (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
+      (* XXX: absorbing anomalies?? *)
+      tclZEROMSG ~info
+        (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
   end
 
 let cutSubstClause l2r eqn cls =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 5fb519cc4f..a0670ef70d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1570,6 +1570,8 @@ let run_hint tac k = match warn_hint () with
   else Proofview.tclTHEN (log_hint tac) (k tac.obj)
 | HintStrict ->
   if is_imported tac then k tac.obj
-  else Proofview.tclZERO (UserError (None, (str "Tactic failure.")))
+  else
+    let info = Exninfo.reify () in
+    Proofview.tclZERO ~info (UserError (None, (str "Tactic failure.")))
 
 let repr_hint h = h.obj
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 374706c8f9..a4d306c497 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -266,22 +266,36 @@ module New = struct
   let tclTHEN t1 t2 =
     t1 <*> t2
 
-  let tclFAIL lvl msg =
-    tclZERO (Refiner.FailError (lvl,lazy msg))
-
-  let tclZEROMSG ?loc msg =
-    let err = UserError (None, msg) in
+  let tclFAIL ?info lvl msg =
+    let info = match info with
+      (* If the backtrace points here it means the caller didn't save
+         the backtrace correctly *)
+      | None -> Exninfo.reify ()
+      | Some info -> info
+    in
+    tclZERO ~info (Refiner.FailError (lvl,lazy msg))
+
+  let tclZEROMSG ?info ?loc msg =
+    let info = match info with
+      (* If the backtrace points here it means the caller didn't save
+         the backtrace correctly *)
+      | None -> Exninfo.reify ()
+      | Some info -> info
+    in
     let info = match loc with
-    | None -> Exninfo.null
-    | Some loc -> Loc.add_loc Exninfo.null loc
+    | None -> info
+    | Some loc -> Loc.add_loc info loc
     in
+    let err = UserError (None, msg) in
     tclZERO ~info err
 
   let catch_failerror e =
     try
       Refiner.catch_failerror e;
       tclUNIT ()
-    with e when CErrors.noncritical e -> tclZERO e
+    with e when CErrors.noncritical e ->
+      let _, info = Exninfo.capture e in
+      tclZERO ~info e
 
   (* spiwack: I chose to give the Ltac + the same semantics as
      [Proofview.tclOR], however, for consistency with the or-else
@@ -441,8 +455,10 @@ module New = struct
 
   (* Try the first tactic that does not fail in a list of tactics *)
   let rec tclFIRST = function
-    | [] -> tclZEROMSG (str"No applicable tactic.")
-    |  t::rest -> tclORELSE0 t (tclFIRST rest)
+    | [] ->
+      let info = Exninfo.reify () in
+      tclZEROMSG ~info (str"No applicable tactic.")
+    | t::rest -> tclORELSE0 t (tclFIRST rest)
 
   let rec tclFIRST_PROGRESS_ON tac = function
     | []    -> tclFAIL 0 (str "No applicable tactic")
@@ -451,7 +467,8 @@ module New = struct
 
   let rec tclDO n t =
     if n < 0 then
-      tclZEROMSG (str"Wrong argument : Do needs a positive integer.")
+      let info = Exninfo.reify () in
+      tclZEROMSG ~info (str"Wrong argument : Do needs a positive integer.")
     else if n = 0 then tclUNIT ()
     else if n = 1 then t
     else tclTHEN t (tclDO (n-1) t)
@@ -474,7 +491,8 @@ module New = struct
   let tclCOMPLETE t =
     t >>= fun res ->
       (tclINDEPENDENT
-         (tclZEROMSG (str"Proof is not complete."))
+         (let info = Exninfo.reify () in
+          tclZEROMSG ~info (str"Proof is not complete."))
       ) <*>
         tclUNIT res
 
@@ -533,7 +551,8 @@ module New = struct
                   let () = check_evars env sigma_final sigma sigma_initial in
                   tclUNIT x
                 with e when CErrors.noncritical e ->
-                  tclZERO e
+                  let e, info = Exninfo.capture e in
+                  tclZERO ~info e
           else
             tclUNIT x
         in
@@ -552,7 +571,8 @@ module New = struct
       (Proofview.tclTIMEOUT n t)
       begin function (e, info) -> match e with
         | Logic_monad.Tac_Timeout as e ->
-          Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e)))
+          let info = Exninfo.reify () in
+          Proofview.tclZERO ~info (Refiner.FailError (0,lazy (CErrors.print e)))
         | e -> Proofview.tclZERO ~info e
       end
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 01565169ca..eebe702259 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -151,9 +151,9 @@ module New : sig
   (* [tclFAIL n msg] fails with [msg] as an error message at level [n]
      (meaning that it will jump over [n] error catching tacticals FROM
      THIS MODULE. *)
-  val tclFAIL : int -> Pp.t -> 'a tactic
+  val tclFAIL : ?info:Exninfo.info -> int -> Pp.t -> 'a tactic
 
-  val tclZEROMSG : ?loc:Loc.t -> Pp.t -> 'a tactic
+  val tclZEROMSG : ?info:Exninfo.info -> ?loc:Loc.t -> Pp.t -> 'a tactic
   (** Fail with a [User_Error] containing the given message. *)
 
   val tclOR : unit tactic -> unit tactic -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 378b6c7418..5fe87a94c5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -182,10 +182,13 @@ let convert_gen pb x y =
   Proofview.Goal.enter begin fun gl ->
     match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with
     | Some sigma -> Proofview.Unsafe.tclEVARS sigma
-    | None -> Tacticals.New.tclFAIL 0 (str "Not convertible")
-    | exception _ ->
+    | None ->
+      let info = Exninfo.reify () in
+      Tacticals.New.tclFAIL ~info 0 (str "Not convertible")
+    | exception e ->
+      let _, info = Exninfo.capture e in
       (* FIXME: Sometimes an anomaly is raised from conversion *)
-      Tacticals.New.tclFAIL 0 (str "Not convertible")
+      Tacticals.New.tclFAIL ~info 0 (str "Not convertible")
 end
 
 let convert x y = convert_gen Reduction.CONV x y
@@ -301,7 +304,9 @@ let rename_hyp repl =
   let init = Some (Id.Set.empty, Id.Set.empty) in
   let dom = List.fold_left fold init repl in
   match dom with
-  | None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping")
+  | None ->
+    let info = Exninfo.reify () in
+    Tacticals.New.tclZEROMSG ~info (str "Not a one-to-one name mapping")
   | Some (src, dst) ->
     Proofview.Goal.enter begin fun gl ->
       let hyps = Proofview.Goal.hyps gl in
@@ -1023,7 +1028,10 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
           (Proofview.Unsafe.tclEVARS sigma)
           (intro_then_gen name_flag move_flag force_flag dep_flag tac)
     | _ ->
-        begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct))
+        begin if not force_flag
+          then
+            let info = Exninfo.reify () in
+            Proofview.tclZERO ~info (RefinerError (env, sigma, IntroNeedsProduct))
             (* Note: red_in_concl includes betaiotazeta and this was like *)
             (* this since at least V6.3 (a pity *)
             (* that intro do betaiotazeta only when reduction is needed; and *)
@@ -1035,7 +1043,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
              (intro_then_gen name_flag move_flag false dep_flag tac))
           begin function (e, info) -> match e with
             | RefinerError (env, sigma, IntroNeedsProduct) ->
-                Tacticals.New.tclZEROMSG (str "No product even after head-reduction.")
+              Tacticals.New.tclZEROMSG ~info (str "No product even after head-reduction.")
             | e -> Proofview.tclZERO ~info e
           end
   end
@@ -1314,7 +1322,8 @@ let cut c =
        know the relevance *)
     match Typing.sort_of env sigma c with
     | exception e when noncritical e ->
-      Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
+      let _, info = Exninfo.capture e in
+      Tacticals.New.tclZEROMSG ~info (str "Not a proposition or a type.")
     | sigma, s ->
       let r = Sorts.relevance_of_sort s in
       let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in
@@ -1666,7 +1675,9 @@ let descend_in_conjunctions avoid tac (err, info) c =
             let env = Proofview.Goal.env gl in
             let sigma = Tacmach.New.project gl in
             match make_projection env sigma params cstr sign elim i n c u with
-            | None -> Tacticals.New.tclFAIL 0 (mt())
+            | None ->
+              let info = Exninfo.reify () in
+              Tacticals.New.tclFAIL ~info 0 (mt())
             | Some (p,pt) ->
               Tacticals.New.tclTHENS
                 (assert_before_gen false (NamingAvoid avoid) pt)
@@ -1718,7 +1729,8 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
         let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
         Clenvtac.res_pf clause ~with_evars ~flags
       with exn when noncritical exn ->
-        Proofview.tclZERO exn
+        let exn, info = Exninfo.capture exn in
+        Proofview.tclZERO ~info exn
     in
     let rec try_red_apply thm_ty (exn0, info) =
       try
@@ -1730,9 +1742,10 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
           | PretypeError _|RefinerError _|UserError _|Failure _ ->
             Some (try_red_apply red_thm (exn0, info))
           | _ -> None)
-      with Redelimination ->
+      with Redelimination as exn ->
         (* Last chance: if the head is a variable, apply may try
             second order unification *)
+        let exn, info = Exninfo.capture exn in
         let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in
         let tac =
           if with_destruct then
@@ -1991,7 +2004,9 @@ let assumption =
     if only_eq then
       let hyps = Proofview.Goal.hyps gl in
       arec gl false hyps
-    else Tacticals.New.tclZEROMSG (str "No such assumption.")
+    else
+      let info = Exninfo.reify () in
+      Tacticals.New.tclZEROMSG ~info (str "No such assumption.")
   | decl::rest ->
     let t = NamedDecl.get_type decl in
     let concl = Proofview.Goal.concl gl in
@@ -2087,12 +2102,13 @@ let clear_body ids =
           else sigma
         in
         Proofview.Unsafe.tclEVARS sigma
-      with DependsOnBody where ->
+      with DependsOnBody where as exn ->
+        let _, info = Exninfo.capture exn in
         let msg = match where with
         | None -> str "Conclusion" ++ on_the_bodies ids
         | Some id -> str "Hypothesis " ++ Id.print id ++ on_the_bodies ids
         in
-        Tacticals.New.tclZEROMSG msg
+        Tacticals.New.tclZEROMSG ~info msg
     in
     check <*>
     Refine.refine ~typecheck:false begin fun sigma ->
@@ -2306,7 +2322,8 @@ let intro_decomp_eq ?loc l thin tac id =
       (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l)
       (eq,t,eq_args) (c, t)
   | None ->
-    Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
+    let info = Exninfo.reify () in
+    Tacticals.New.tclZEROMSG ~info (str "Not a primitive equality here.")
   end
 
 let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
@@ -3992,13 +4009,14 @@ let specialize_eqs id =
         (internal_cut true id ty')
         (exact_no_check ((* refresh_universes_strict *) acc'))
     else
-      Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ Id.print id)
+      let info = Exninfo.reify () in
+      Tacticals.New.tclFAIL ~info 0 (str "Nothing to do in hypothesis " ++ Id.print id)
   end
 
 let specialize_eqs id = Proofview.Goal.enter begin fun gl ->
   let msg = str "Specialization not allowed on dependent hypotheses" in
   Proofview.tclOR (clear [id])
-    (fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () ->
+    (fun (_,info) -> Tacticals.New.tclZEROMSG ~info msg) >>= fun () ->
     specialize_eqs id
 end
 
@@ -4414,7 +4432,8 @@ let induction_without_atomization isrec with_evars elim names lid =
     scheme.nargs + (if scheme.farg_in_concl then 1 else 0) in
   if not (Int.equal (List.length lid) (scheme.nparams + nargs_indarg_farg))
   then
-    Tacticals.New.tclZEROMSG (msg_not_right_number_induction_arguments scheme)
+    let info = Exninfo.reify () in
+    Tacticals.New.tclZEROMSG ~info (msg_not_right_number_induction_arguments scheme)
   else
   let indvars,lid_params = List.chop nargs_indarg_farg lid in
   (* terms to patternify we must patternify indarg or farg if present in concl *)
@@ -4528,7 +4547,8 @@ let guard_no_unifiable = Proofview.guard_no_unifiable >>= function
   | Some l ->
     Proofview.tclENV     >>= function env ->
     Proofview.tclEVARMAP >>= function sigma ->
-    Proofview.tclZERO (RefinerError (env, sigma, UnresolvedBindings l))
+    let info = Exninfo.reify () in
+    Proofview.tclZERO ~info (RefinerError (env, sigma, UnresolvedBindings l))
 
 let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
      id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac =
@@ -4831,7 +4851,9 @@ let reflexivity_red allowred =
     let sigma = Tacmach.New.project gl in
     let concl = maybe_betadeltaiota_concl allowred gl in
     match match_with_equality_type env sigma concl with
-    | None -> Proofview.tclZERO NoEquationFound
+    | None ->
+      let info = Exninfo.reify () in
+      Proofview.tclZERO ~info NoEquationFound
     | Some _ -> one_constructor 1 NoBindings
   end
 
@@ -4873,8 +4895,9 @@ let match_with_equation c =
   try
     let res = match_with_equation env sigma c in
     Proofview.tclUNIT res
-  with NoEquationFound ->
-    Proofview.tclZERO NoEquationFound
+  with NoEquationFound as exn ->
+    let _, info = Exninfo.capture exn in
+    Proofview.tclZERO ~info NoEquationFound
 
 let symmetry_red allowred =
   Proofview.Goal.enter begin fun gl ->
@@ -4987,7 +5010,9 @@ let transitivity_red allowred t =
           | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t])
    | None,eq,eq_kind ->
       match t with
-      | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.")
+      | None ->
+        let info = Exninfo.reify () in
+        Tacticals.New.tclZEROMSG ~info (str"etransitivity not supported for this relation.")
       | Some t -> prove_transitivity eq eq_kind t
   end
 
@@ -5005,8 +5030,8 @@ let transitivity t = transitivity_gen (Some t)
 let intros_transitivity  n  = Tacticals.New.tclTHEN intros (transitivity_gen n)
 
 let constr_eq ~strict x y =
-  let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in
-  let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in
+  let fail ~info = Tacticals.New.tclFAIL ~info 0 (str "Not equal") in
+  let fail_universes ~info = Tacticals.New.tclFAIL ~info 0 (str "Not equal (due to universes)") in
   Proofview.Goal.enter begin fun gl ->
     let env = Tacmach.New.pf_env gl in
     let evd = Tacmach.New.project gl in
@@ -5015,13 +5040,18 @@ let constr_eq ~strict x y =
         let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in
         if strict then
           if Evd.check_constraints evd csts then Proofview.tclUNIT ()
-          else fail_universes
+          else
+            let info = Exninfo.reify () in
+            fail_universes ~info
         else
           (match Evd.add_constraints evd csts with
            | evd -> Proofview.Unsafe.tclEVARS evd
-           | exception Univ.UniverseInconsistency _ ->
-             fail_universes)
-      | None -> fail
+           | exception (Univ.UniverseInconsistency _ as e) ->
+             let _, info = Exninfo.capture e in
+             fail_universes ~info)
+      | None ->
+        let info = Exninfo.reify () in
+        fail ~info
   end
 
 let unify ?(state=TransparentState.full) x y =
@@ -5042,7 +5072,8 @@ let unify ?(state=TransparentState.full) x y =
     let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in
     Proofview.Unsafe.tclEVARS sigma
   with e when noncritical e ->
-    Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None)))
+    let e, info = Exninfo.capture e in
+    Proofview.tclZERO ~info (PretypeError (env, sigma, CannotUnify (x, y, None)))
   end
 
 (** [tclWRAPFINALLY before tac finally] runs [before] before each
diff --git a/user-contrib/Ltac2/tac2match.ml b/user-contrib/Ltac2/tac2match.ml
index 22f65507c1..86c7b0e3be 100644
--- a/user-contrib/Ltac2/tac2match.ml
+++ b/user-contrib/Ltac2/tac2match.ml
@@ -131,7 +131,9 @@ module PatternMatching (E:StaticEnvironment) = struct
     { stream = fun k ctx -> m.stream (fun () ctx -> y.stream k ctx) ctx }
 
   (** Failure of the pattern-matching monad: no success. *)
-  let fail (type a) : a m = { stream = fun _ _ -> Proofview.tclZERO matching_error }
+  let fail (type a) : a m = { stream = fun _ _ ->
+      let info = Exninfo.reify () in
+      Proofview.tclZERO ~info matching_error }
 
   let run (m : 'a m) =
     let ctx = {
@@ -150,7 +152,11 @@ module PatternMatching (E:StaticEnvironment) = struct
 
   let put_subst subst : unit m =
     let s = { subst } in
-    { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s }
+    { stream = fun k ctx -> match merge s ctx with
+          | None ->
+            let info = Exninfo.reify () in
+            Proofview.tclZERO ~info matching_error
+          | Some s -> k () s }
 
   (** {6 Pattern-matching} *)