diff options
| author | Maxime Dénès | 2019-01-17 10:53:19 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-21 10:26:04 +0100 |
| commit | 945f49236e0db8179548110a056f9787ecffd746 (patch) | |
| tree | c3c350f7f6279cab7bd572069ce3846be77145fe /kernel/nativecode.mli | |
| parent | 10a9c492a486fcb884ffeadd1d05ecb0fae90d0f (diff) | |
At Qed, if shelved goals remain, emit a warning instead of an error
This error was more or less a debug tool (checking that no tactic breaks
the invariant). But some users may want to support other models, see
https://github.com/Mtac2/Mtac2/pull/139 for an example discussion.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions