From 1f3ea50258490ac8b5a395ac0ff2bca7326e755f Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 12 May 2015 17:55:10 +0200
Subject: Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)

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

(limited to 'theories/Classes')

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 1a40e5d59..15cb02d37 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