From ca1a22c3dd8d098b7a9ca2d84cb8ea3fceef075a Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:08:54 +0000
Subject: simplification in deps of some g_*.ml4

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15377 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_proofs.ml4 | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

(limited to 'parsing/g_proofs.ml4')

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 22a9e0d85f..2086bfffcf 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -6,19 +6,17 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pcoq
-open Pp
-open Tactic
-open Util
-open Vernac_
 open Constrexpr
 open Vernacexpr
 open Locality
-open Prim
-open Constr
-open Tok
 open Misctypes
 
+open Pcoq
+open Pcoq.Tactic
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Vernac_
+
 let thm_token = G_vernac.thm_token
 
 (* Proof commands *)
-- 
cgit v1.2.3