diff options
| -rw-r--r-- | pretyping/evarsolve.ml | 7 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4240.v | 12 |
2 files changed, 19 insertions, 0 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index bfd19c6c7..b2cf21b81 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -157,6 +157,7 @@ let restrict_evar_key evd evk filter candidates = end (* Restrict an applied evar and returns its restriction in the same context *) +(* (the filter is assumed to be at least stronger than the original one) *) let restrict_applied_evar evd (evk,argsv) filter candidates = let evd,newevk = restrict_evar_key evd evk filter candidates in let newargsv = match filter with @@ -885,6 +886,9 @@ let filter_candidates evd evk filter candidates_update = else UpdateWith l' +(* Given a filter refinement for the evar [evk], restrict it so that + dependencies are preserved *) + let closure_of_filter evd evk = function | None -> None | Some filter -> @@ -892,8 +896,11 @@ let closure_of_filter evd evk = function let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in let test b (id,c,_) = b || Idset.mem id vars || match c with None -> false | Some c -> not (isRel c || isVar c) in let newfilter = Filter.map_along test filter (evar_context evi) in + (* Now ensure that restriction is at least what is was originally *) + let newfilter = Option.cata (Filter.map_along (&&) newfilter) newfilter (Filter.repr (evar_filter evi)) in if Filter.equal newfilter (evar_filter evi) then None else Some newfilter +(* The filter is assumed to be at least stronger than the original one *) let restrict_hyps evd evk filter candidates = (* What to do with dependencies? Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y. diff --git a/test-suite/bugs/closed/4240.v b/test-suite/bugs/closed/4240.v new file mode 100644 index 000000000..083c59fe6 --- /dev/null +++ b/test-suite/bugs/closed/4240.v @@ -0,0 +1,12 @@ +(* Check that closure of filter did not restrict the former evar filter *) + +Lemma foo (new : nat) : False. +evar (H1: nat). +set (H3 := 0). +assert (H3' := id H3). +evar (H5: nat). +clear H3. +assert (H5 = new). +unfold H5. +unfold H1. +exact (eq_refl new). |