From f461e7657cab9917c5b405427ddba3d56f197efb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 8 May 2016 18:59:55 +0200
Subject: Removing dead code and unused opens.

---
 interp/notation.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index b8f4f32017..0a65dfc096 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -13,7 +13,6 @@ open Pp
 open Bigint
 open Names
 open Term
-open Nametab
 open Libnames
 open Globnames
 open Constrexpr
-- 
cgit v1.2.3