From 37cc37090fcbabb9546a79558c9420e532701be4 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 31 Dec 2015 20:07:06 +0100 Subject: Put implicits back as in 8.4. --- theories/Classes/RelationClasses.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'theories/Classes') diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 15cb02d37..6248babd0 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -208,6 +208,10 @@ Hint Extern 4 (subrelation (flip _) _) => class_apply @subrelation_symmetric : typeclass_instances. Arguments irreflexivity {A R Irreflexive} [x] _. +Arguments symmetry {A} {R} {_} [x] [y] _. +Arguments asymmetry {A} {R} {_} [x] [y] _ _. +Arguments transitivity {A} {R} {_} [x] [y] [z] _ _. +Arguments Antisymmetric A eqA {_} _. Hint Resolve irreflexivity : ord. -- cgit v1.2.3