diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-14 20:56:29 +0530 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-18 00:16:42 +0530 |
commit | f5cb0571c85a6fa61f25f92626f1752fc3fd6c34 (patch) | |
tree | 6bbca1e53920b3d3e15a3130b3dd3a540d0c2afd /theories/Classes/RelationPairs.v | |
parent | ed339b1eef52a73e6e170b2613e65c1037105132 (diff) |
Remove typeclass opaque directive, some proofs in the stdlib rely on it being transparent
Diffstat (limited to 'theories/Classes/RelationPairs.v')
-rw-r--r-- | theories/Classes/RelationPairs.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index 8ce3e4b6b..cbde5f9ab 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. |