diff options
| author | Matthieu Sozeau | 2019-09-12 11:41:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-12-14 12:21:20 +0100 |
| commit | 40323e4258d5232226d0be277f53bb5462bac417 (patch) | |
| tree | e0d8baa2ba8a0f4bd4695c1c0703b3c243b906c0 /kernel | |
| parent | dd47dfc29f4b38dd2b1745ecbf452c3cd459b89b (diff) | |
Fix refine and eapply to mark shelved goals as non-resolvable, always
Check that we don't regress on PR #10762 example
Fix regression discovered by Arthur in PR #10762
Fix script of #10298 which was relying on breaking semantics for `eapply`
Add doc
Add comment in clenvtac
Actually, always mark shelved goals as unresolvable
Update doc to reflect semantics w.r.t. shelved subgoals
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions