From 6ce9f50c6f516696236fa36e5ff190142496798f Mon Sep 17 00:00:00 2001
From: notin
Date: Thu, 6 Mar 2008 15:46:06 +0000
Subject: Coquille vraisemblablement introduite par la révision 10628

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10630 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Classes/Morphisms.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index fb0acb39ca..1ba1f585ae 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -421,5 +421,5 @@ Qed.
 Instance {A : Type} (m : A -> Prop) =>
   any_eq_iff_morphism : Morphism (@Logic.eq A ==> iff) m | 4.
 Proof.
-  red ; intros. subst ; reflexivity.
+  red ; intros. subst ; split; trivial.
 Qed.
-- 
cgit v1.2.3