From 32bcb10ce3470377314b964223ce9aed1ab33c72 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 10 Oct 2011 13:31:13 +0000
Subject: Proper fix for complement/flip instances.

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

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index f798ad68af..04688b00f9 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -236,7 +236,7 @@ Program Definition complement_proper
     intuition.
   Qed.
  
-Hint Extern 1 (Proper (_ ==> _ ==> _) (complement _)) => 
+Hint Extern 1 (Proper _ (complement _)) => 
   apply @complement_proper : typeclass_instances.
 
 (** The [inverse] too, actually the [flip] instance is a bit more general. *)
@@ -250,7 +250,7 @@ Program Definition flip_proper
     apply mor ; auto.
   Qed.
 
-Hint Extern 1 (Proper (_ ==> _ ==> _) (flip _)) => 
+Hint Extern 1 (Proper _ (flip _)) => 
   apply @flip_proper : typeclass_instances.
 
 (** Every Transitive relation gives rise to a binary morphism on [impl],
-- 
cgit v1.2.3