Optimizing evar filters. It seems to cost quite a lot in unification,

as witnessed by profiling on time-consuming files. I suspect we can
do better by using a smarter representation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16912 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 5 insertions, 6 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b4388ff089..44138a8ee1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -720,7 +720,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
         | Some _ -> error "Selection of specific occurrences not supported"
         | None ->
         let evty = set_holes evdref cty subst in
-        let _, instance = List.filter2 (fun b c -> b) filter instance in
+        let instance = List.filter_with filter instance in
         let evd,ev = new_evar_instance sign !evdref evty ~filter instance in
         evdref := evd;
         evsref := (fst (destEvar ev),evty)::!evsref;
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index c8122c4dc5..7ae44faf8a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -45,7 +45,7 @@ let test_success conv_algo env evd c c' rhs =
 (************************)
 
 let extract_subfilter initial_filter refined_filter =
-  snd (List.filter2 (fun b1 b2 -> b1) initial_filter refined_filter)
+  List.filter_with initial_filter refined_filter
 
 let apply_subfilter filter subfilter =
   fst (List.fold_right (fun oldb (l,filter) ->
@@ -82,7 +82,7 @@ let restrict_evar_key evd evk filter candidates =
       let sign = evar_hyps evi in
       let src = evi.evar_source in
       let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in
-      let _, ctxt = List.filter2 (fun b c -> b) filter (evar_context evi) in
+      let ctxt = List.filter_with filter (evar_context evi) in
       let id_inst = Array.of_list (List.map (fun (id,_,_) -> mkVar id) ctxt) in
       Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk
     end
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 920fb54180..de394e6609 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -239,8 +239,7 @@ let non_instantiated sigma =
 (* Manipulating filters *)
 (************************)
 
-let extract_subfilter initial_filter refined_filter =
-  snd (List.filter2 (fun b1 b2 -> b1) initial_filter refined_filter)
+let extract_subfilter = List.filter_with
 
 let make_pure_subst evi args =
   snd (List.fold_right
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index df02975ce5..751809bc55 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -57,7 +57,7 @@ let evar_filter evi = evi.evar_filter
 let evar_body evi = evi.evar_body
 let evar_context evi = named_context_of_val evi.evar_hyps
 let evar_filtered_context evi =
-  snd (List.filter2 (fun b c -> b) (evar_filter evi) (evar_context evi))
+  List.filter_with (evar_filter evi) (evar_context evi)
 let evar_hyps evi = evi.evar_hyps
 let evar_filtered_hyps evi =
   List.fold_right push_named_context_val (evar_filtered_context evi)