diff options
| author | Gaëtan Gilbert | 2018-11-28 16:18:46 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-28 16:18:46 +0100 |
| commit | 58e5071189bf60aadb35aaafb7016615557be7de (patch) | |
| tree | 7b0d5daac68596c30158e3848e7566d90c1d3bda | |
| parent | 2e36fbcac4a04d4f29925ba09f441db6426b7af1 (diff) | |
| parent | abdc6b34b11ac1ccbcb8c48291b74c6762fc7573 (diff) | |
Merge PR #7153: Make OrderedTypeFullFacts a module functor
| -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 60c64d306b..1fb0a37e16 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. |