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

2 files changed, 17 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.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 8e491b1b8..30d82822a 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -146,6 +146,13 @@ Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
   Next Obligation.
   Proof with auto.
     assert(R x0 x0).
+    transitivity y0... symmetry... 
+    symmetry... apply H1. now symmetry.
+  Qed.
+
+  Next Obligation.
+  Proof with auto.
+    assert(R x0 x0).
     transitivity y0... symmetry...
     transitivity (y x0)...
   Qed.