diff options
| author | letouzey | 2006-04-05 11:56:14 +0000 |
|---|---|---|
| committer | letouzey | 2006-04-05 11:56:14 +0000 |
| commit | 004484f8406428df8c9ce0852d1c083a9125c3dc (patch) | |
| tree | fe68e4a23e2024b1bf96e20d3cdeee3153c10413 /theories | |
| parent | 8f4f8a3e60f8b708b1a8fbb9495d972d11c06609 (diff) | |
on utilise explicitement Prop/iff pour certains morphismes pour eviter des warnings
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8681 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/FSets/FSetFacts.v | 6 | ||||
| -rw-r--r-- | theories/FSets/FSetWeakFacts.v | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index 835ae610a4..0edb009cf3 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -295,7 +295,7 @@ Qed. Add Setoid t Equal Equal_ST as EqualSetoid. -Add Morphism In : In_m. +Add Morphism In with signature E.eq ==> Equal ==> iff as In_m. Proof. unfold Equal; intros x y H s s' H0. rewrite (In_eq_iff s H); auto. @@ -318,7 +318,7 @@ destruct H1 as (_,H1). exact (H1 (refl_equal true) _ Ha). Qed. -Add Morphism Empty : Empty_m. +Add Morphism Empty with signature Equal ==> iff as Empty_m. Proof. intros; do 2 rewrite is_empty_iff; rewrite H; intuition. Qed. @@ -367,7 +367,7 @@ unfold Equal; intros s s' H s'' s''' H0 a. do 2 rewrite diff_iff; rewrite H; rewrite H0; intuition. Qed. -Add Morphism Subset : Subset_m. +Add Morphism Subset with signature Equal ==> Equal ==> iff as Subset_m. Proof. unfold Equal, Subset; firstorder. Qed. diff --git a/theories/FSets/FSetWeakFacts.v b/theories/FSets/FSetWeakFacts.v index c35eef3a27..c5e82e09c8 100644 --- a/theories/FSets/FSetWeakFacts.v +++ b/theories/FSets/FSetWeakFacts.v @@ -299,7 +299,7 @@ Qed. Add Setoid t Equal Equal_ST as EqualSetoid. -Add Morphism In : In_m. +Add Morphism In with signature E.eq ==> Equal ==> iff as In_m. Proof. unfold Equal; intros x y H s s' H0. rewrite (In_eq_iff s H); auto. @@ -322,7 +322,7 @@ destruct H1 as (_,H1). exact (H1 (refl_equal true) _ Ha). Qed. -Add Morphism Empty : Empty_m. +Add Morphism Empty with signature Equal ==> iff as Empty_m. Proof. intros; do 2 rewrite is_empty_iff; rewrite H; intuition. Qed. @@ -373,7 +373,7 @@ unfold Equal; intros s s' H s'' s''' H0 a. do 2 rewrite diff_iff; rewrite H; rewrite H0; intuition. Qed. -Add Morphism Subset : Subset_m. +Add Morphism Subset with signature Equal ==> Equal ==> iff as Subset_m. Proof. unfold Equal, Subset; firstorder. Qed. |