diff options
| author | Pierre-Marie Pédrot | 2017-09-09 20:40:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-09 20:40:11 +0200 |
| commit | a059c181c3b2d6c1f9c3682c15270c0942430f39 (patch) | |
| tree | ac85208fe717887ab81846390da422c17f923a2a /kernel/type_errors.mli | |
| parent | 254785a4a7f8373b5b0c4a289c2184cac3b5c420 (diff) | |
Fix coq/ltac2#18: Terms should show a backtrace when Set Ltac2 Backtrace is set.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions