cList: a few alternative to hashtbl-based uniquize, distinct, subset

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

1 files changed, 7 insertions, 4 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index fc5fc0d2c0..aa8f2d08ea 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -781,17 +781,20 @@ let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
  * such that "hyps' |- ?e : T"
  *)
 
+let set_of_evctx l =
+  List.fold_left (fun s (id,_,_) -> Id.Set.add id s) Id.Set.empty l
+
 let filter_candidates evd evk filter candidates =
   let evi = Evd.find_undefined evd evk in
   let candidates = match candidates with
   | None -> evi.evar_candidates
-  | Some _ -> candidates in
+  | Some _ -> candidates
+  in
   match candidates,filter with
   | None,_ | _, None -> candidates
   | Some l, Some filter ->
-      let ids = List.map pi1 (List.filter_with filter (evar_context evi)) in
-      Some (List.filter (fun a ->
-        List.subset (Id.Set.elements (collect_vars a)) ids) l)
+      let ids = set_of_evctx (List.filter_with filter (evar_context evi)) in
+      Some (List.filter (fun a -> Id.Set.subset (collect_vars a) ids) l)
 
 let eq_filter f1 f2 =
   let eq_bool b1 b2 = if b1 then b2 else not b2 in