From 3bd82b3cb10a721f2e2c8db6d0271c83a22095a3 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 13 Feb 2017 11:15:34 +0100
Subject: Use "Local" as prefix

Open Local becomes Local Open.  This silences Coq 8.6's warning.
Also: remove one useless Require-inside-a-module that caused another warning.
---
 lib/Lattice.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib/Lattice.v')

diff --git a/lib/Lattice.v b/lib/Lattice.v
index 4455e22f..6eebca99 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -56,7 +56,7 @@ End SEMILATTICE.
 
 Module Type SEMILATTICE_WITH_TOP.
 
-  Include Type SEMILATTICE.
+  Include SEMILATTICE.
   Parameter top: t.
   Axiom ge_top: forall x, ge top x.
 
-- 
cgit