diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index a7957ebe8..d71499eda 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) |