diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-11-27 09:28:09 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-11-28 19:21:24 +0100 |
| commit | 34815f0c8fae4c87798b18f7343c1f1afc3056eb (patch) | |
| tree | daaa3b44d5ae0016a6cbfb78f9582b170c080568 /lib/option.mli | |
| parent | 5d3f5c210aad8d73b007936e65694c401e66c7d0 (diff) | |
Tactic primitives: missing [advance] lead to spurious dangling goals.
Closes #3801.
Diffstat (limited to 'lib/option.mli')
0 files changed, 0 insertions, 0 deletions