diff options
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/Init.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index 8b4cac5f4e..7fb48aa433 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -33,7 +33,7 @@ Class Unconvertible (A : Type) (a b : A). Ltac unconvertible := match goal with - | |- @Unconvertible _ ?x ?y => conv x y ; fail 1 "Convertible" + | |- @Unconvertible _ ?x ?y => unify x y with typeclass_instances ; fail 1 "Convertible" | |- _ => eapply Build_Unconvertible end. |