diff options
Diffstat (limited to 'theories/Classes/RelationClasses.v')
| -rw-r--r-- | theories/Classes/RelationClasses.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index bdd7b4b1d..dcf3139b2 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -23,12 +23,13 @@ Require Export Coq.Relations.Relation_Definitions. (** We allow to unfold the [relation] definition while doing morphism search. *) -Typeclasses unfold relation. - Notation inverse R := (flip (R:relation _) : relation _). Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False. +(** Opaque for proof-search. *) +Typeclasses Opaque complement. + (** These are convertible. *) Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R). |