aboutsummaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cases.ml')
-rw-r--r--pretyping/cases.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 57725dbdc1..3b904570d4 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1709,8 +1709,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in
begin
let flags = (default_flags_of TransparentState.full) in
- let conv = conv_fun evar_conv_x flags in
- match solve_simple_eqn conv !!env sigma (None,ev,substl inst ev') with
+ match solve_simple_eqn evar_unify flags !!env sigma (None,ev,substl inst ev') with
| Success evd -> evdref := evd
| UnifFailure _ -> assert false
end;