Tentative to fix bug #2628 by not letting intuition break records. Might be too much of a backwards-incompatible change

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14949 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 1 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index d9e9fe257..87316cda9 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -115,6 +115,12 @@ Section Respecting.
 
   Next Obligation.
   Proof.
+    unfold respecting in *. program_simpl. transitivity (y y0); auto. symmetry; apply H. reflexivity.
+  Qed.
+
+
+  Next Obligation.
+  Proof.
     unfold respecting in *. program_simpl. transitivity (y y0); auto. apply H0. reflexivity.
   Qed.
 
@@ -122,10 +128,13 @@ End Respecting.
 
 (** The default equivalence on function spaces, with higher-priority than [eq]. *)
 
+Hint Extern 0 => reflexivity : relations.
+Hint Extern 1 => solve [symmetry; auto] : relations.
+
 Program Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) :
   Equivalence (pointwise_relation A eqB) | 9.
 
   Next Obligation.
   Proof.
-    transitivity (y a) ; auto.
+    transitivity (y a); auto with relations.
   Qed.