diff options
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/RelationClasses.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 61edb2b98..3bd9dcd12 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -202,6 +202,8 @@ Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_insta Hint Extern 4 (subrelation (flip _) _) => class_apply @subrelation_symmetric : typeclass_instances. +Arguments irreflexivity {A R Irreflexive} [x] _. + Hint Resolve irreflexivity : ord. Unset Implicit Arguments. |