Better representation of evar filters: we represent the vacuous filters of

any length with a [None] representation and ensure that this representation
is canonical through the restricted interface.

1 files changed, 3 insertions, 3 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a7957ebe84..d71499eda9 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1573,12 +1573,12 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
 	  (fun i _ -> if Int.List.mem i vl then u else mkRel i) 1
 	  (rel_context extenv) in
       let rel_filter =
-	Filter.init_list (fun a -> not (isRel a) || dependent a u
+	List.map (fun a -> not (isRel a) || dependent a u
                            || Int.Set.mem (destRel a) depvl) inst in
       let named_filter =
-	Filter.init_list (fun (id,_,_) -> dependent (mkVar id) u)
+	List.map (fun (id,_,_) -> dependent (mkVar id) u)
 	  (named_context extenv) in
-      let filter = Filter.append rel_filter named_filter in
+      let filter = Filter.make (rel_filter @ named_filter) in
       let candidates = u :: List.map mkRel vl in
       let ev =
 	e_new_evar evdref extenv ~src:(loc, Evar_kinds.CasesType)