From abdc6b34b11ac1ccbcb8c48291b74c6762fc7573 Mon Sep 17 00:00:00 2001
From: Simon Gregersen
Date: Mon, 2 Apr 2018 20:21:20 +0200
Subject: Make OrderedTypeFullFacts a module functor

---
 theories/Structures/OrdersFacts.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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.
-- 
cgit v1.2.3