[exn] [tactics] improve backtraces on monadic errors

Current backtraces for tactics leave a bit to desire, for example
given the program:

```coq
Lemma u n : n + 0 = n.
rewrite plus_O_n.
```

the backtrace stops at:

```
Found no subterm matching "0 + ?M160" in the current goal.
Called from file "proofs/proof.ml", line 381, characters 4-42
Called from file "tactics/pfedit.ml", line 102, characters 31-58
Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84
```

Backtrace information `?info` is as of today optional in some tactics,
such as `tclZERO`, it doesn't cost a lot  however to reify backtrace
information indeed in `tclZERO` and provide backtraces for all tactic
errors. The cost should be small if we are not in debug mode.

The backtrace for the failed rewrite is now:

```
Found no subterm matching "0 + ?M160" in the current goal.
Raised at file "pretyping/unification.ml", line 1827, characters 14-73
Called from file "pretyping/unification.ml", line 1929, characters 17-53
Called from file "pretyping/unification.ml", line 1948, characters 22-72
Called from file "pretyping/unification.ml", line 2020, characters 14-56
Re-raised at file "pretyping/unification.ml", line 2021, characters 66-73
Called from file "proofs/clenv.ml", line 254, characters 12-58
Called from file "proofs/clenvtac.ml", line 95, characters 16-53
Called from file "engine/proofview.ml", line 1110, characters 40-46
Called from file "engine/proofview.ml", line 1115, characters 10-34
Re-raised at file "clib/exninfo.ml", line 82, characters 4-38
Called from file "proofs/proof.ml", line 381, characters 4-42
Called from file "tactics/pfedit.ml", line 102, characters 31-58
Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84
```

which IMO is much better.

12 files changed, 183 insertions, 88 deletions

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