From 3840dbd43398e5ff6ed7dbbc1cc6b19ec2eddb97 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 1 Jun 2017 15:47:47 +0200
Subject: Remove a post merge warning.

---
 library/nameops.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/library/nameops.ml b/library/nameops.ml
index b73bd7eb38..0b5dfd8d0e 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Util
 open Names
 
-- 
cgit v1.2.3