diff options
| author | Pierre-Marie Pédrot | 2018-06-28 15:35:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-05 12:09:41 +0100 |
| commit | 785d2008988d73d2ec1c93940d9c93084d1acbbc (patch) | |
| tree | 0bf2a134ece83333e54304438f051ef65212884d /dev | |
| parent | 740ec848acc0b127fad7ba5b703bc00364126c71 (diff) | |
Add an option not to register Ltac backtraces.
Fixes #7769: Better control over ltac backtraces.
Fixes #7385: Tactic allocates gigabytes of RAM.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions