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 | |
| 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')
| -rw-r--r-- | engine/proofview.ml | 7 | ||||
| -rw-r--r-- | engine/proofview.mli | 9 |
2 files changed, 12 insertions, 4 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 diff --git a/engine/proofview.mli b/engine/proofview.mli index 8ec53ac78c..a92179ab5b 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -481,8 +481,13 @@ module Unsafe : sig and makes them unresolvable for type classes. *) val mark_as_goals : Evd.evar_map -> Evar.t list -> Evd.evar_map - (** Make an evar unresolvable for type classes. *) - val mark_as_unresolvable : proofview -> Evar.t -> proofview + (** Make some evars unresolvable for type classes. + We need two functions as some functions use the proofview and others + directly manipulate the undelying evar_map. + *) + val mark_unresolvables : Evd.evar_map -> Evar.t list -> Evd.evar_map + + val mark_as_unresolvables : proofview -> Evar.t list -> proofview (** [advance sigma g] returns [Some g'] if [g'] is undefined and is the current avatar of [g] (for instance [g] was changed by [clear] |