aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cases.ml')
-rw-r--r--pretyping/cases.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c0141f011..01e2db08c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1690,7 +1690,6 @@ let abstract_tycon loc env evdref subst tycon extenv t =
(named_context extenv) in
let filter = Filter.make (rel_filter @ named_filter) in
let candidates = u :: List.map mkRel vl in
- let candidates = List.map EConstr.Unsafe.to_constr candidates in
let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in
lift k ev
in