diff options
| author | Simon Gregersen | 2018-04-02 20:21:20 +0200 |
|---|---|---|
| committer | Simon Gregersen | 2018-04-02 20:21:20 +0200 |
| commit | abdc6b34b11ac1ccbcb8c48291b74c6762fc7573 (patch) | |
| tree | d0224fb59e0efe65c32c5e0963b2093c2473efb5 /theories/Structures | |
| parent | f29f8f80c8ad94576c7a36f3f638866c208338a0 (diff) | |
Make OrderedTypeFullFacts a module functor
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/OrdersFacts.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 87df6b479d..f6bf6401f8 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -77,7 +77,7 @@ End CompareFacts. (** * Properties of [OrderedTypeFull] *) -Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull'). +Module OrderedTypeFullFacts (Import O:OrderedTypeFull'). Module OrderTac := OTF_to_OrderTac O. Ltac order := OrderTac.order. |