diff options
| author | Arnaud Spiwack | 2014-08-05 16:49:13 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-05 16:58:52 +0200 |
| commit | 6458868b7ba2eb04cad7bf670dda6ba4f01f7c80 (patch) | |
| tree | 181bc2a7c050cc33740dca176e080d8f24f23482 /stm/asyncTaskQueue.ml | |
| parent | 5f9b15657dacd258fbd9084424afd4aa96929f3f (diff) | |
Ring: prevent an error message to show in case of success.
Since [idtac] can, now, be used even if no goal is left, this error message which assumed that the goal was still open would run at every call of the [ring] tactic. Which lead to comically many nonsensical messages on the console during Coq's compilation.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions