From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 14 Oct 2010 17:51:11 +0200 Subject: Imported Upstream version 8.3 --- theories/Classes/RelationClasses.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'theories/Classes/RelationClasses.v') diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 1aad3cec..2bfebfd8 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -15,7 +15,7 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id: RelationClasses.v 13344 2010-07-28 15:04:36Z msozeau $ *) +(* $Id: RelationClasses.v 13476 2010-09-30 11:42:11Z letouzey $ *) Require Export Coq.Classes.Init. Require Import Coq.Program.Basics. @@ -149,9 +149,9 @@ Program Instance iff_Transitive : Transitive iff. (** Leibniz equality. *) -Program Instance eq_Reflexive : Reflexive (@eq A). -Program Instance eq_Symmetric : Symmetric (@eq A). -Program Instance eq_Transitive : Transitive (@eq A). +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