diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 77007b0ba..8963ea5ea 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1489,9 +1489,9 @@ let abstract_tycon loc env evdref subst _tycon extenv t = List.map (fun (id,_,_) -> dependent (mkVar id) u) (named_context extenv) in let filter = rel_filter@named_filter in + let candidates = u :: List.map mkRel vl in let ev = - e_new_evar evdref extenv ~src:(loc, CasesType) ~filter:filter ty in - evdref := add_conv_pb (Reduction.CONV,extenv,substl inst ev,u) !evdref; + e_new_evar evdref extenv ~src:(loc, CasesType) ~filter ~candidates ty in lift k ev else map_constr_with_full_binders push_binder aux x t in |