Abstracting evar filter away. The API is not perfect, but better than nothing.

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

1 files changed, 3 insertions, 3 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d2f53e953f..6381c29a16 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -339,7 +339,7 @@ let new_evar evd env ?src ?filter ?candidates typ =
   let instance =
     match filter with
     | None -> instance
-    | Some filter -> List.filter_with filter instance in
+    | Some filter -> Filter.filter_list filter instance in
   new_evar_instance sign evd typ' ?src ?filter ?candidates instance
 
 let new_type_evar ?src ?filter evd env =
@@ -651,7 +651,7 @@ let define_pure_evar_as_product evd evk =
   let evd2,rng =
     let newenv = push_named (id, None, dom) evenv in
     let src = evar_source evk evd1 in
-    let filter = true::evar_filter evi in
+    let filter = Filter.cons true (evar_filter evi) in
     new_type_evar evd1 newenv ~src ~filter in
   let prod = mkProd (Name id, dom, subst_var id rng) in
   let evd3 = Evd.define evk prod evd2 in
@@ -689,7 +689,7 @@ let define_pure_evar_as_lambda env evd evk =
   let id =
     next_name_away_with_default_using_types "x" na avoid (whd_evar evd dom) in
   let newenv = push_named (id, None, dom) evenv in
-  let filter = true::evar_filter evi in
+  let filter = Filter.cons true (evar_filter evi) in
   let src = evar_source evk evd1 in
   let evd2,body = new_evar evd1 newenv ~src (subst1 (mkVar id) rng) ~filter in
   let lam = mkLambda (Name id, dom, subst_var id body) in