diff options
| author | Hugo Herbelin | 2014-10-08 19:25:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-08 19:47:40 +0200 |
| commit | 827a2bba4c9342a50c47ce257b40cb395518be6f (patch) | |
| tree | cd0260bc4d6990f133f6b9205a04de9a475bf0e3 /pretyping | |
| parent | 335cf2860bfd9e714d14228d75a52fd2c88db386 (diff) | |
Fixing the anomaly in bug #3045 (a filter was not type-safe in
2nd-order matching).
We made the filter type-safe (i.e. to ensure that Gamma |- ?n:T is
well-typed when taking the filtered context Gamma) in 2nd order
matching. Maybe this weakens the power of the 2nd order matching
algorithm, so it is not clear that it is the good fix.
Another fix could have been to ensure that taking the closure of
filter does not extend it beyond the original filter (hence keeping
the filter untyped if it was already untyped).
As for the bug #3045, it also revealed that some "destruct c as [[]]"
could be made stronger as decomposing the destruct in two parts
"destruct c as [x]; destruct x" workis while it currently fails if in
one part.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6946279838..19e405b80d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -838,8 +838,11 @@ let apply_on_subterm env evdref f c t = applyrec (env,(0,c)) t let filter_possible_projections c ty ctxt args = - let fv1 = free_rels c in - let fv2 = collect_vars c in + (* Since args in the types will be replaced by holes, we count the + fv of args to have a well-typed filter; don't know how necessary + it is however to have a well-typed filter here *) + let fv1 = free_rels (mkApp (c,args)) (* Hack: locally untyped *) in + let fv2 = collect_vars (mkApp (c,args)) in let len = Array.length args in let tyvars = collect_vars ty in List.map_i (fun i (id,b,_) -> |