From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Fri, 13 Nov 2015 11:31:34 +0100
Subject: Imported Upstream version 8.5~beta3+dfsg

---
 theories/Classes/RelationClasses.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'theories/Classes/RelationClasses.v')

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 1a40e5d5..15cb02d3 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -89,6 +89,11 @@ Section Defs.
   Global Instance Equivalence_PER {R} `(E:Equivalence R) : PER R | 10 :=
     { }. 
 
+  (** An Equivalence is a PreOrder plus symmetry. *)
+
+  Global Instance Equivalence_PreOrder {R} `(E:Equivalence R) : PreOrder R | 10 :=
+    { }.
+
   (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
   
   Class Antisymmetric eqA `{equ : Equivalence eqA} (R : relation A) :=
-- 
cgit v1.2.3