diff options
| author | msozeau | 2008-09-04 10:47:27 +0000 |
|---|---|---|
| committer | msozeau | 2008-09-04 10:47:27 +0000 |
| commit | 589effd34254f5082e522821de9af93e54cdaf86 (patch) | |
| tree | d72d8b3d154a62986091b5025866facecfa86e05 /theories/Classes | |
| parent | 39f6bc84e726a6e3e09644b5b7e38c3c3475972b (diff) | |
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
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/RelationClasses.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 9c5b757818..cfcd93c0a4 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -392,4 +392,4 @@ Program Instance subrelation_partial_order : Qed. Typeclasses Opaque arrows predicate_implication predicate_equivalence - relation_equivalence. + relation_equivalence pointwise_lifting. |