diff options
| author | Pierre-Marie Pédrot | 2017-09-09 20:45:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-09 20:46:02 +0200 |
| commit | 6bc632021b47103b57abb34836766a57198d9cb4 (patch) | |
| tree | 4ddb0538aae3e61a725726a42efe20b39176c5d7 /src/tac2stdlib.ml | |
| parent | 91a9313fbe24dfb0c9b7fcaa31e3c11bf055450a (diff) | |
Update backtraces only when the Ltac2 Backtrace flag is set.
Diffstat (limited to 'src/tac2stdlib.ml')
0 files changed, 0 insertions, 0 deletions