[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.

1 files changed, 31 insertions, 18 deletions

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 =