From 6dae53d279afe2b8dcfc43dd2aded9431944c5c8 Mon Sep 17 00:00:00 2001
From: regisgia
Date: Fri, 14 Sep 2012 15:59:23 +0000
Subject: This patch removes unused "open" (automatically generated from
 compiler warnings).

I was afraid that such a brutal refactoring breaks some obscure
invariant about linking order and side-effects but the standard
library still compiles.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/egramcoq.ml | 3 ---
 parsing/egramml.ml  | 1 -
 parsing/extrawit.ml | 1 -
 3 files changed, 5 deletions(-)

(limited to 'parsing')

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 4cfc730a92..488c425cc5 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Compat
 open Errors
 open Util
@@ -15,11 +14,9 @@ open Extend
 open Ppextend
 open Constrexpr
 open Notation_term
-open Genarg
 open Libnames
 open Tacexpr
 open Names
-open Vernacexpr
 open Egramml
 
 (**************************************************************************)
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index abd1bcd5b5..c74f369075 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Compat
 open Names
 open Pcoq
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml
index 75205c9644..e7d9ba4b2f 100644
--- a/parsing/extrawit.ml
+++ b/parsing/extrawit.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Errors
-open Util
 open Genarg
 
 (* This file defines extra argument types *)
-- 
cgit v1.2.3