From ba92fdf0422503d7b69c3cd02d67a4dcee408d64 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 4 Jan 2015 15:41:34 +0100
Subject: Fixing old filter bug in second_order_matching.

---
 pretyping/evarconv.ml | 4 +---
 1 file changed, 1 insertion(+), 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
 
-- 
cgit v1.2.3