diff options
| author | Hugo Herbelin | 2015-01-04 15:41:34 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-06 14:19:13 +0100 |
| commit | ba92fdf0422503d7b69c3cd02d67a4dcee408d64 (patch) | |
| tree | 9c9656002301a70e0b076ef4c71cacfa288e20ab | |
| parent | 3895a86c1f00bd7c935e31998914b467f0866a35 (diff) | |
Fixing old filter bug in second_order_matching.
| -rw-r--r-- | pretyping/evarconv.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a5d11fbfb1..9f0e47c6ce 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -975,7 +975,6 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let env_evar = evar_filtered_env evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in - let filter = evar_filter evi in let instance = List.map mkVar (List.map pi1 ctxt) in let rec make_subst = function @@ -990,8 +989,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let evs = ref [] in let ty = Retyping.get_type_of env_rhs evd c in let filter' = filter_possible_projections c ty ctxt args in - let filter = Filter.map_along (&&) filter filter' in - (id,t,c,ty,evs,filter,occs) :: make_subst (ctxt',l,occsl) + (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) | _, _, [] -> [] | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in |