diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Classes/Init.v | 2 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 2 |
2 files changed, 2 insertions, 2 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. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index eb5c7cc11f..fff78a85af 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -93,7 +93,7 @@ Ltac clear_dup := | [ H' : ?Y |- _ ] => match H with | H' => fail 2 - | _ => conv X Y ; (clear H' || clear H) + | _ => unify X Y ; (clear H' || clear H) end end end. |