From e792b4a6b0a9a279293ff7ff5748bc61d2116ce6 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 22 Oct 2013 17:26:28 +0000
Subject: 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
---
 lib/cList.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'lib')

diff --git a/lib/cList.ml b/lib/cList.ml
index 643ef7f2bd..2cc5e4cfd3 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -600,11 +600,11 @@ let map_filter_i f =
         match f i x with None -> l' | Some y -> y::l'
   in aux 0
 
-let filter_along f filter l =
-  snd (filter2 (fun b c -> f b) filter l)
-
-let filter_with filter l =
-  filter_along (fun x -> x) filter l
+let rec filter_with filter l = match filter, l with
+| [], [] -> []
+| true :: filter, x :: l -> x :: filter_with filter l
+| false :: filter, _ :: l -> filter_with filter l
+| _ -> invalid_arg "List.filter_with"
 
 let subset l1 l2 =
   let t2 = Hashtbl.create 151 in
-- 
cgit v1.2.3