diff options
Diffstat (limited to 'theories/FSets/FSetDecide.v')
| -rw-r--r-- | theories/FSets/FSetDecide.v | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index 82c684634..b7a1deb77 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -19,10 +19,10 @@ Require Import Decidable DecidableTypeEx FSetFacts. -(** First, a version for Weak Sets *) +(** First, a version for Weak Sets in functorial presentation *) -Module WDecide (E : DecidableType)(Import M : WSfun E). - Module F := FSetFacts.WFacts E M. +Module WDecide_fun (E : DecidableType)(Import M : WSfun E). + Module F := FSetFacts.WFacts_fun E M. (** * Overview This functor defines the tactic [fsetdec], which will @@ -851,15 +851,14 @@ the above form: End FSetDecideTestCases. -End WDecide. +End WDecide_fun. Require Import FSetInterface. -(** Now comes a special version dedicated to full sets. For this - one, only one argument [(M:S)] is necessary. *) +(** Now comes variants for self-contained weak sets and for full sets. + For these variants, only one argument is necessary. Thanks to + the subtyping [WS<=S], the [Decide] functor which is meant to be + used on modules [(M:S)] can simply be an alias of [WDecide]. *) -Module Decide (M : S). - Module D:=OT_as_DT M.E. - Module WD := WDecide D M. - Ltac fsetdec := WD.fsetdec. -End Decide.
\ No newline at end of file +Module WDecide (M:WS) := WDecide_fun M.E M. +Module Decide := WDecide. |