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 /doc/changelog | |
| 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 'doc/changelog')
| -rw-r--r-- | doc/changelog/04-tactics/10762-notypeclasses-refine.rst | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst new file mode 100644 index 0000000000..2fef75dc7f --- /dev/null +++ b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst @@ -0,0 +1,4 @@ +- **Changed:** + The tactics :tacn:`eapply`, :tacn:`refine` and its variants no + longer allows shelved goals to be solved by typeclass resolution. + (`#10762 <https://github.com/coq/coq/pull/10762>`_, by Matthieu Sozeau). |