From e8bde450d05908f70ab2c82d9d24f0807c56a94a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 4 Mar 2020 21:39:42 -0500
Subject: [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.
---
 user-contrib/Ltac2/tac2match.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'user-contrib')

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} *)
 
-- 
cgit v1.2.3