From 4ddddba01d49ba7c019ebb0444cd58c18c8ad40d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 14 Jan 2015 20:56:29 +0530
Subject: Remove typeclass opaque directive, some proofs in the stdlib rely on
 it being transparent

---
 theories/Classes/RelationPairs.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index 8ce3e4b6b7..cbde5f9ab5 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -42,7 +42,6 @@ Generalizable Variables A B RA RB Ri Ro f.
 
 Definition RelCompFun {A} {B : Type}(R:relation B)(f:A->B) : relation A :=
  fun a a' => R (f a) (f a').
-Typeclasses Opaque RelCompFun.
 
 Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope.
 
-- 
cgit v1.2.3