diff options
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. |