diff options
| -rw-r--r-- | theories/FSets/FSetDecide.v | 3 | ||||
| -rw-r--r-- | theories/FSets/FSetEqProperties.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FSetProperties.v | 2 |
3 files changed, 4 insertions, 3 deletions
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index e8d639003..fe6623c33 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -22,6 +22,7 @@ Require Import Decidable DecidableTypeEx FSetFacts. (** First, a version for Weak Sets *) Module WDecide (E : DecidableType)(Import M : WSfun E). + Module F := FSetFacts.WFacts E M. (** * Overview This functor defines the tactic [fsetdec], which will @@ -462,7 +463,7 @@ the above form: the predicates [In] and [E.eq] applied only to variables. We are going to use them with [autorewrite]. *) - Module F := FSetFacts.WFacts E M. + Hint Rewrite F.empty_iff F.singleton_iff F.add_iff F.remove_iff F.union_iff F.inter_iff F.diff_iff diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index 55cfd7e7c..41034ce85 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -21,7 +21,7 @@ Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx. Module WEqProperties (Import E:DecidableType)(M:WSfun E). Module Import MP := WProperties E M. -Import FM. +Import FM Dec.F. Import M. Definition Add := MP.Add. diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 1ea669eb8..d64cab173 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -29,8 +29,8 @@ Hint Extern 1 (Setoid_Theory _ _) => constructor; congruence. should take two arguments in order to compensate this. *) Module WProperties (Import E : DecidableType)(M : WSfun E). - Module Import FM := WFacts E M. Module Import Dec := WDecide E M. + Module Import FM := Dec.F (* FSetFacts.WFacts E M *). Import M. Lemma In_dec : forall x s, {In x s} + {~ In x s}. |