diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-05 15:24:38 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-05 15:24:38 +0000 |
| commit | 41138b8f14d17f3c409d592c18e5a4def664a2e8 (patch) | |
| tree | 53e61dcd72940f85a085c51d5dc579ffa84a0d86 /theories/MSets/MSetEqProperties.v | |
| parent | f4ceaf2ce34c5cec168275dee3e7a99710bf835f (diff) | |
Avoid declaring hints about refl/sym/trans of eq in DecidableType2
This used to be convenient in FSets, but since we now try to integrate
DecidableType and OrderedType as foundation for other part of the stdlib,
this should be avoided, otherwise some eauto take a _long_ time.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12626 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/MSets/MSetEqProperties.v')
| -rw-r--r-- | theories/MSets/MSetEqProperties.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v index 49f436a01..fe6c3c79c 100644 --- a/theories/MSets/MSetEqProperties.v +++ b/theories/MSets/MSetEqProperties.v @@ -89,7 +89,7 @@ Qed. Lemma add_mem_1: mem x (add x s)=true. Proof. -auto with set. +auto with set relations. Qed. Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s. @@ -99,7 +99,7 @@ Qed. Lemma remove_mem_1: mem x (remove x s)=false. Proof. -rewrite <- not_mem_iff; auto with set. +rewrite <- not_mem_iff; auto with set relations. Qed. Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s. @@ -275,7 +275,7 @@ Qed. Lemma singleton_mem_1: mem x (singleton x)=true. Proof. -auto with set. +auto with set relations. Qed. Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false. @@ -653,7 +653,7 @@ Lemma filter_add_1 : forall s x, f x = true -> Proof. red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff. intuition. -rewrite <- H; apply Comp; auto. +rewrite <- H; apply Comp; auto with relations. Qed. Lemma filter_add_2 : forall s x, f x = false -> @@ -672,7 +672,7 @@ unfold Add, MP.Add; intros. repeat rewrite filter_iff; auto. rewrite H0; clear H0. intuition. -setoid_replace y with x; auto. +setoid_replace y with x; auto with relations. Qed. Lemma add_filter_2 : forall s s' x, @@ -908,9 +908,9 @@ elim (equal_2 H x); auto with set; intros. apply fold_equal with (eqA:=eqA); auto with set. transitivity (f x (fold f s0 i)). apply fold_add with (eqA:=eqA); auto with set. -transitivity (g x (fold f s0 i)); auto with set. -transitivity (g x (fold g s0 i)); auto with set. -apply gc; auto with set. +transitivity (g x (fold f s0 i)); auto with set relations. +transitivity (g x (fold g s0 i)); auto with set relations. +apply gc; auto with set relations. symmetry; apply fold_add with (eqA:=eqA); auto. do 2 rewrite fold_empty; reflexivity. Qed. |