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.

---
 parsing/egramcoq.ml  | 2 --
 parsing/egramml.ml   | 2 --
 parsing/g_vernac.ml4 | 1 -
 parsing/pcoq.ml      | 1 -
 4 files changed, 6 deletions(-)

(limited to 'parsing')

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index f0c12ab8ef..04b6228643 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -14,9 +14,7 @@ open Extend
 open Constrexpr
 open Notation_term
 open Libnames
-open Tacexpr
 open Names
-open Egramml
 
 (**************************************************************************)
 (*
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 37fccdb3c2..95ac872473 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Util
-open Compat
-open Names
 open Extend
 open Pcoq
 open Genarg
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 1c39858ea7..35ba9757d4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -20,7 +20,6 @@ open Misctypes
 open Tok (* necessary for camlp4 *)
 
 open Pcoq
-open Pcoq.Tactic
 open Pcoq.Prim
 open Pcoq.Constr
 open Pcoq.Vernac_
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 53d2089c04..fe9ab630fa 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -12,7 +12,6 @@ open Errors
 open Util
 open Extend
 open Genarg
-open Tok (* necessary for camlp4 *)
 
 (** The parser of Coq *)
 
-- 
cgit v1.2.3