From 9ba0a98c3fdfa197ef9becc9eb1144a56bf5a036 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 17 Feb 2010 13:44:37 +0000
Subject: RelationClasses: adapt eq_Reflexive and co to avoid Universe
 Inconsistencies

 We explicitely take care of the argument A to be given to eq_refl,sym,trans
 when proving that Logic.eq is an instance of Equivalence. This should solve
 the recent Universe Inconsistencies encountered in CoLoR and FingerTree.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12786 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Classes/RelationClasses.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index e4fcf2eb15..0d9c9ae9d5 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -149,9 +149,9 @@ Program Instance iff_Transitive : Transitive iff.
 
 (** Leibniz equality. *)
 
-Instance eq_Reflexive : Reflexive (@eq A) := eq_refl.
-Instance eq_Symmetric : Symmetric (@eq A) := eq_sym.
-Instance eq_Transitive : Transitive (@eq A) := eq_trans.
+Instance eq_Reflexive {A} : Reflexive (@eq A) := @eq_refl A.
+Instance eq_Symmetric {A} : Symmetric (@eq A) := @eq_sym A.
+Instance eq_Transitive {A} : Transitive (@eq A) := @eq_trans A.
 
 (** Various combinations of reflexivity, symmetry and transitivity. *)
 
-- 
cgit v1.2.3