global_reference migrated from Libnames to new Globnames, less deps in grammar.cma

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 10 insertions, 12 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3ac5b87ba..3263de8d5 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -19,7 +19,6 @@ open Vernacexpr
 open Locality
 open Decl_kinds
 open Genarg
-open Ppextend
 open Goptions
 open Declaremods
 open Misctypes
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 50270f863..7387f6933 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -16,6 +16,7 @@ open Glob_term
 open Genarg
 open Tacexpr
 open Libnames
+open Globnames
 
 open Nametab
 open Detyping
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index 226ef4b36..27ca281c8 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -14,15 +14,10 @@ Dyn
 Hashcons
 Predicate
 Option
-Hashtbl_alt
 
 Names
 Univ
-Esubst
-Term
-Mod_subst
 
-Nameops
 Libnames
 Summary
 Genarg
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index ba3def1a0..4034252db 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -19,7 +19,6 @@ open Topconstr
 open Genarg
 open Tacexpr
 open Extrawit
-open Ppextend
 
 (** The parser of Coq *)
 
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 6e9f475a3..15acfd718 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -89,7 +89,7 @@ let pr_located pr (loc,x) = pr x
 
 let pr_evaluable_reference = function
   | EvalVarRef id -> pr_id id
-  | EvalConstRef sp -> pr_global (Libnames.ConstRef sp)
+  | EvalConstRef sp -> pr_global (Globnames.ConstRef sp)
 
 let pr_quantified_hypothesis = function
   | AnonHyp n -> int n
@@ -314,7 +314,7 @@ let pr_ltac_constant sp =
 let pr_evaluable_reference_env env = function
   | EvalVarRef id -> pr_id id
   | EvalConstRef sp ->
-      Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.ConstRef sp)
+      Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp)
 
 let pr_esubst prc l =
   let pr_qhyp = function
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index f1f6db64d..f4c53333f 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -29,6 +29,7 @@ open Libobject
 open Printer
 open Printmod
 open Libnames
+open Globnames
 open Nametab
 open Recordops
 open Misctypes
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 122da7ebf..d6bec7162 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -15,6 +15,7 @@ open Term
 open Environ
 open Reductionops
 open Libnames
+open Globnames
 open Nametab
 open Misctypes
 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index a932a608f..8754b9129 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -17,6 +17,7 @@ open Environ
 open Global
 open Declare
 open Libnames
+open Globnames
 open Nametab
 open Evd
 open Proof_type
diff --git a/parsing/printer.mli b/parsing/printer.mli
index bbc3a6cad..77e4db79e 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -9,6 +9,7 @@
 open Pp
 open Names
 open Libnames
+open Globnames
 open Term
 open Sign
 open Environ
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index cf047bfa3..d81802ac2 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Declarations
 open Nameops
+open Globnames
 open Libnames
 open Goptions
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index cb4fad6f5..7467a32f0 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -8,7 +8,6 @@
 
 open Pp
 open Names
-open Libnames
 open Q_util
 open Compat
 
@@ -39,8 +38,8 @@ let mlexpr_of_dirpath dir =
   <:expr< Names.make_dirpath $mlexpr_of_list mlexpr_of_ident l$ >>
 
 let mlexpr_of_qualid qid =
-  let (dir, id) = repr_qualid qid in
-  <:expr< make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >>
+  let (dir, id) = Libnames.repr_qualid qid in
+  <:expr< Libnames.make_qualid $mlexpr_of_dirpath dir$ $mlexpr_of_ident id$ >>
 
 let mlexpr_of_reference = function
   | Libnames.Qualid (loc,qid) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >>