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.

---
 plugins/quote/g_quote.ml4 | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'plugins/quote')

diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index e4c8da93b1..fd87d5b7d3 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -14,9 +14,6 @@ open Tacexpr
 open Geninterp
 open Quote
 open Constrarg
-open Pcoq.Prim
-open Pcoq.Constr
-open Pcoq.Tactic
 
 DECLARE PLUGIN "quote_plugin"
 
-- 
cgit v1.2.3