diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/Typeclasses.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index dfa438d90a..3eaa04144f 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -5,7 +5,7 @@ Record Equ (A : Type) (R : A -> A -> Prop). Definition equiv {A} R (e : Equ A R) := R. Record Refl (A : Type) (R : A -> A -> Prop). Axiom equ_refl : forall A R (e : Equ A R), Refl _ (@equiv A R e). -Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [|shelve|] : foo. +Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [shelve|] : foo. Variable R : nat -> nat -> Prop. Lemma bas : Equ nat R. |