diff options
| author | Emilio Jesus Gallego Arias | 2020-03-04 21:39:42 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-14 21:31:56 +0200 |
| commit | e8bde450d05908f70ab2c82d9d24f0807c56a94a (patch) | |
| tree | 4db3de0ae89817423a7e2f664beb62240a81d9cd /tactics/autorewrite.ml | |
| parent | cc54af3842cbf99f169f7937b0e31f737652bd3a (diff) | |
[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.
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 7 |
1 files changed, 5 insertions, 2 deletions
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)) = |