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_ltac.ml4   | 10 ++++------
 parsing/g_prim.ml4   |  9 +++------
 parsing/g_proofs.ml4 | 14 ++++++--------
 3 files changed, 13 insertions(+), 20 deletions(-)

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index c8356b6033..f5bf5e099c 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -7,19 +7,17 @@
 (************************************************************************)
 
 open Pp
-open Util
 open Constrexpr
-open Glob_term
 open Tacexpr
 open Vernacexpr
 open Locality
-open Pcoq
-open Prim
-open Tactic
-open Tok
 open Misctypes
 open Genredexpr
 
+open Pcoq
+open Pcoq.Prim
+open Pcoq.Tactic
+
 let fail_default_value = ArgArg 0
 
 let arg_of_expr = function
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index d6b2d83803..7a058bd871 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -6,18 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pcoq
 open Names
 open Libnames
-open Topconstr
-open Tok
-open Compat
+
+open Pcoq
+open Pcoq.Prim
 
 let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
 let _ = List.iter Lexer.add_keyword prim_kw
 
-open Prim
-open Nametab
 
 let local_make_qualid l id = make_qualid (make_dirpath l) id
 
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