diff options
| author | Maxime Dénès | 2019-12-17 11:16:49 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-12-17 11:16:49 +0100 |
| commit | 7cf4ba4026e8ffd27684a9685b2972f30d2308de (patch) | |
| tree | d71bd065d33faec6cfa99241ff1d63e5e6b5219d /engine | |
| parent | 82918ec41ccab3b1623e41139b448938f4760a80 (diff) | |
| parent | 40323e4258d5232226d0be277f53bb5462bac417 (diff) | |
Merge PR #10762: Fix refine and eapply to mark shelved goals as non-resolvable, always
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
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] |