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

Indeed it is breaking too many scripts.
This reverts commit 47e9afaaa4c08aca97d4f4b5a89cb40da76bd850.

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

2 files changed, 1 insertions, 17 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 87316cda9..d9e9fe257 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -115,12 +115,6 @@ 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.
 
@@ -128,13 +122,10 @@ 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 with relations.
+    transitivity (y a) ; auto.
   Qed.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 30d82822a..8e491b1b8 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -146,13 +146,6 @@ 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.