Library Coq.ssr.ssrclasses
Compatibility layer for
under and
setoid_rewrite.
Note: this file does not require
ssreflect; it is both required by
ssrsetoid and required by
ssrunder.
Redefine
Coq.Classes.RelationClasses.Reflexive here, so that doing
Require Import ssreflect does not
Require Import RelationClasses,
and conversely.
Section Defs.
Context {A : Type}.
Class Reflexive (R : A -> A -> Prop) :=
reflexivity : forall x : A, R x x.
End Defs.
Instance eq_Reflexive {A : Type} : Reflexive (@eq A) := @eq_refl A.
Instance iff_Reflexive : Reflexive iff := iff_refl.