Major speed and space improvements in setoid rewrite:

- Avoid using projections for singleton classes. Divides the size
  of proofs by 2 and simplifies the typechecking as well.
- Switch to the new discrimination net implementation for classes, 
  with the current convention that all constants are unfoldable. 
  Users can add "Typeclasses Opaque" declarations make the dnet 
  discriminate more, otherwise it should be entirely
  backward-compatible.
- Fix bug introduced in r11333 in "transitivity" tactic in presence
  of coercions.
Up to 15% gains on setoid-intensive files like Ring_polynom and
Field_theory. More importantly, performance should not decrease
significantly by adding new Morphism/Setoid declarations.


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

1 files changed, 6 insertions, 3 deletions

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index dcf3139b2..80592d136 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -69,15 +69,15 @@ Program Instance flip_Irreflexive [ Irreflexive A R ] : Irreflexive (flip R) :=
 
 Program Instance flip_Symmetric [ Symmetric A R ] : Symmetric (flip R).
 
-  Solve Obligations using unfold flip ; program_simpl ; clapply Symmetric.
+  Solve Obligations using unfold flip ; program_simpl ; typeclass_app Symmetric.
 
 Program Instance flip_Asymmetric [ Asymmetric A R ] : Asymmetric (flip R).
   
-  Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry.
+  Solve Obligations using program_simpl ; unfold flip in * ; intros ; typeclass_app asymmetry ; eauto.
 
 Program Instance flip_Transitive [ Transitive A R ] : Transitive (flip R).
 
-  Solve Obligations using unfold flip ; program_simpl ; clapply transitivity.
+  Solve Obligations using unfold flip ; program_simpl ; typeclass_app transitivity ; eauto.
 
 Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A) ]
    : Irreflexive (complement R).
@@ -390,3 +390,6 @@ Program Instance subrelation_partial_order :
   Proof.
     unfold relation_equivalence in *. firstorder.
   Qed.
+
+Typeclasses Opaque arrows predicate_implication predicate_equivalence 
+  relation_equivalence.