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 /engine/proofview.ml | |
| 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 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index ed44372045..6f8e668e4e 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1025,8 +1025,11 @@ module Unsafe = struct let undefined = undefined - let mark_as_unresolvable p gl = - { p with solution = mark_in_evm ~goal:false p.solution [gl] } + let mark_unresolvables evm evs = + mark_in_evm ~goal:false evm evs + + let mark_as_unresolvables p evs = + { p with solution = mark_in_evm ~goal:false p.solution evs } end |