Improve typeclasses eauto using the dnet for local assumptions too, and select

only relevant hypotheses in it, slightly cutting the search space. 
Makes setoid_rewrite less sensitive to the number of hypothesis (~ 5%
time improvment on the stdlib). This currently prevents resolution with
constants which reduce to classes, hence the modifications in Setoids.Setoid.


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

1 files changed, 14 insertions, 8 deletions

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 8f59c048f..28d8feeae 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -12,14 +12,20 @@ Require Export Coq.Classes.SetoidTactics.
 
 (** For backward compatibility *)
 
-Definition Setoid_Theory := @Equivalence.  
-Definition Build_Setoid_Theory := @Build_Equivalence.  
-Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x :=
-  Eval compute in reflexivity.
-Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x :=
-  Eval compute in symmetry.
-Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z :=
-  Eval compute in transitivity.
+Definition Setoid_Theory := @Equivalence.
+Definition Build_Setoid_Theory := @Build_Equivalence.
+
+Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x.
+  unfold Setoid_Theory. intros ; reflexivity.
+Defined.
+
+Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x.
+  unfold Setoid_Theory. intros ; symmetry ; assumption.
+Defined.
+
+Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z.
+  unfold Setoid_Theory. intros ; transitivity y ; assumption.
+Defined.
 
 (** Some tactics for manipulating Setoid Theory not officially 
     declared as Setoid. *)