From d82e4cc31064b543ba68f0f52a1c60128da0e539 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 9 Apr 2008 09:18:14 +0000
Subject: Fix the last compilation problem

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

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index fd8576a8cd..17f8970fc9 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -132,7 +132,6 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq
 
   Next Obligation.
   Proof.
-    red.
     extensionality x.
     destruct x ; auto.
   Qed.
-- 
cgit v1.2.3