diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-30 17:05:38 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-30 17:05:38 +0000 |
| commit | 14071a88408b2a678c8129aebf90e669eee007ee (patch) | |
| tree | c4e1d3e0660afe1f3503ab1fae006d37f50878a2 /theories/FSets | |
| parent | 5dc1e83de7d933dccd9b8590b77e1c3d4cec593c (diff) | |
temporary workaround for bug #1738
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10278 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets')
| -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. |