diff options
| author | Pierre-Marie Pédrot | 2017-09-07 23:45:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-08 01:36:52 +0200 |
| commit | bdd594093b4fb7e46a6cae0135b6630d75bae6f6 (patch) | |
| tree | 7c59b547c765f61d3de89e6cc71283694089d9d8 /kernel | |
| parent | 643832c053e0255dd356231f4e5887db0228c2cd (diff) | |
Fix coq/ltac2#22: Argument to Tactic_failure should be printed.
We implement a printer for toplevel values and use it for exceptions in
particular.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions