diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/FSets/FSetFacts.v | 7 | ||||
| -rw-r--r-- | theories/FSets/FSetWeakFacts.v | 7 |
2 files changed, 10 insertions, 4 deletions
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index 4de3480d0..0c494e7c3 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -419,15 +419,18 @@ Qed. (* [Subset] is a setoid order *) Lemma Subset_refl : forall s, s[<=]s. -Proof. red; auto. Qed. +Proof. red; auto. Defined. Lemma Subset_trans : forall s s' s'', s[<=]s'->s'[<=]s''->s[<=]s''. -Proof. unfold Subset; eauto. Qed. +Proof. unfold Subset; eauto. Defined. Add Relation t Subset reflexivity proved by Subset_refl transitivity proved by Subset_trans as SubsetSetoid. +(* NB: for the moment, it is important to use Defined and not Qed in + the two previous lemmas, in order to allow conversion of + SubsetSetoid coming from separate Facts modules. See bug #1738. *) Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m. Proof. diff --git a/theories/FSets/FSetWeakFacts.v b/theories/FSets/FSetWeakFacts.v index 12bef504d..0740d7f8e 100644 --- a/theories/FSets/FSetWeakFacts.v +++ b/theories/FSets/FSetWeakFacts.v @@ -416,15 +416,18 @@ Qed. (* [Subset] is a setoid order *) Lemma Subset_refl : forall s, s[<=]s. -Proof. red; auto. Qed. +Proof. red; auto. Defined. Lemma Subset_trans : forall s s' s'', s[<=]s'->s'[<=]s''->s[<=]s''. -Proof. unfold Subset; eauto. Qed. +Proof. unfold Subset; eauto. Defined. Add Relation t Subset reflexivity proved by Subset_refl transitivity proved by Subset_trans as SubsetSetoid. +(* NB: for the moment, it is important to use Defined and not Qed in + the two previous lemmas, in order to allow conversion of + SubsetSetoid coming from separate Facts modules. See bug #1738. *) Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m. Proof. |