diff options
| author | ppedrot | 2013-10-27 15:02:43 +0000 |
|---|---|---|
| committer | ppedrot | 2013-10-27 15:02:43 +0000 |
| commit | 4c2302a2db3da1095ce9167ad0e4956defd3947f (patch) | |
| tree | f528bcab8e1d39b741cd3b88df74733e37f78c09 /pretyping/cases.ml | |
| parent | d28285fa1c05297c7618a887b1758e283a9ebe64 (diff) | |
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
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 d10a52fcea..bcdfd23097 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1524,12 +1524,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 = - List.map (fun a -> not (isRel a) || dependent a u + Filter.init_list (fun a -> not (isRel a) || dependent a u || Int.Set.mem (destRel a) depvl) inst in let named_filter = - List.map (fun (id,_,_) -> dependent (mkVar id) u) + Filter.init_list (fun (id,_,_) -> dependent (mkVar id) u) (named_context extenv) in - let filter = rel_filter@named_filter in + let filter = Filter.append 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) |