diff options
| author | Hugo Herbelin | 2014-12-07 12:50:26 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-07 15:20:14 +0100 |
| commit | 48509b6112fc857abdfc442c89821363043ac705 (patch) | |
| tree | 7786c30d41f44c7b657c9a4b48e6001392ac52fa | |
| parent | fa906a5137058cf12444c70b76908b959012ce6d (diff) | |
Improving evar restriction (this is a risky change, as I remember a
similar optimization broke at some time some ssreflect code; we now
treat the easy case of a let-in to a rel - a pattern common in
pattern-matching compilation -; later on, we shall want to investigate
whether any let-in found to refer to out of scope rels or vars can be
filtered out).
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/evars.v | 5 |
2 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 2a819a018b..f51a39d9e3 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -870,7 +870,7 @@ let closure_of_filter evd evk = function | Some filter -> let evi = Evd.find_undefined evd evk in let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in - let test b (id,c,_) = b || Idset.mem id vars || not (Option.is_empty c) in + let test b (id,c,_) = b || Idset.mem id vars || match c with None -> false | Some c -> isRel c in let newfilter = Filter.map_along test filter (evar_context evi) in if Filter.equal newfilter (evar_filter evi) then None else Some newfilter diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index ef2164a942..21c72475ed 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -399,3 +399,8 @@ Goal forall x (x':=x) (f:forall y, y=y:>nat -> Prop), f _ (eq_refl x'). intros. unfold x' at 2. (* A way to check that there are indeed 2 occurrences of x' *) Abort. + +(* A simple example we would like not to fail (it used to fail because of + not strict enough evar restriction) *) + +Check match Some _ with None => _ | _ => _ end. |