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

18 files changed, 22 insertions, 13 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 87a5ce73b..38fe7a1ca 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -20,6 +20,7 @@ open Inductive
 open Sign
 open Environ
 open Libnames
+open Globnames
 open Impargs
 open Constrexpr
 open Constrexpr_ops
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 38f8b6579..0c5d4b589 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -13,6 +13,7 @@ open Termops
 open Sign
 open Environ
 open Libnames
+open Globnames
 open Nametab
 open Glob_term
 open Pattern
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 480dc6ce2..5a8dcac08 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -14,6 +14,7 @@ open Names
 open Nameops
 open Namegen
 open Libnames
+open Globnames
 open Impargs
 open Glob_term
 open Glob_ops
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 10fbde605..7c682ec42 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -12,6 +12,7 @@ open Sign
 open Evd
 open Environ
 open Libnames
+open Globnames
 open Glob_term
 open Pattern
 open Constrexpr
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 9eda0b96a..6f01bb466 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -12,6 +12,7 @@ open Pp
 open Names
 open Term
 open Libnames
+open Globnames
 open Pattern
 open Nametab
 open Smartlocate
@@ -125,8 +126,8 @@ let jmeq_module_name = ["Coq";"Logic";"JMeq"]
 let jmeq_module = make_dir jmeq_module_name
 
 (* TODO: temporary hack *)
-let make_kn dir id = Libnames.encode_mind dir id
-let make_con dir id = Libnames.encode_con dir id
+let make_kn dir id = Globnames.encode_mind dir id
+let make_con dir id = Globnames.encode_con dir id
 
 (** Identity *)
 
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 27137e81b..a77b1060c 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Libnames
+open Globnames
 open Nametab
 open Term
 open Pattern
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 5ea9cb986..58577356b 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -102,18 +102,18 @@ let type_of_global_ref gr =
     "class"
   else
     match gr with
-    | Libnames.ConstRef cst ->
+    | Globnames.ConstRef cst ->
 	type_of_logical_kind (Decls.constant_kind cst)
-    | Libnames.VarRef v ->
+    | Globnames.VarRef v ->
 	"var" ^ type_of_logical_kind (Decls.variable_kind v)
-    | Libnames.IndRef ind ->
+    | Globnames.IndRef ind ->
 	let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
 	  if mib.Declarations.mind_record then
 	    if mib.Declarations.mind_finite then "rec"
 	    else "corec"
 	  else if mib.Declarations.mind_finite then "ind"
 	  else "coind"
-    | Libnames.ConstructRef _ -> "constr"
+    | Globnames.ConstructRef _ -> "constr"
 
 let remove_sections dir =
   if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 59a695ee6..16fa04ef9 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -26,7 +26,7 @@ type coqdoc_state = Lexer.location_table
 val coqdoc_freeze : unit -> coqdoc_state
 val coqdoc_unfreeze : coqdoc_state -> unit
 
-val add_glob : Pp.loc -> Libnames.global_reference -> unit
+val add_glob : Pp.loc -> Globnames.global_reference -> unit
 val add_glob_kn : Pp.loc -> Names.kernel_name -> unit
 
 val dump_definition : Pp.loc * Names.identifier -> bool -> string -> unit
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 3986d135a..2bd19632e 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -10,6 +10,7 @@ open Pp
 open Names
 open Term
 open Libnames
+open Globnames
 open Glob_term
 open Genredexpr
 open Pattern
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index d6e7485dc..90b495982 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -20,6 +20,7 @@ open Util
 open Glob_term
 open Constrexpr
 open Libnames
+open Globnames
 open Typeclasses
 open Typeclasses_errors
 open Pp
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 3d869a019..6297a17d2 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -18,6 +18,7 @@ open Glob_term
 open Constrexpr
 open Pp
 open Libnames
+open Globnames
 open Typeclasses
 
 val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit
diff --git a/interp/notation.ml b/interp/notation.ml
index f2dec3bc1..64911675b 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -15,6 +15,7 @@ open Names
 open Term
 open Nametab
 open Libnames
+open Globnames
 open Summary
 open Constrexpr
 open Notation_term
diff --git a/interp/notation.mli b/interp/notation.mli
index d38f3d6bf..668d827f5 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -13,6 +13,7 @@ open Bigint
 open Names
 open Nametab
 open Libnames
+open Globnames
 open Constrexpr
 open Glob_term
 open Notation_term
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index f0a20d648..853c6967c 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -11,7 +11,7 @@ open Errors
 open Util
 open Names
 open Nameops
-open Libnames
+open Globnames
 open Misctypes
 open Glob_term
 open Glob_ops
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 176c2a76b..06a73723b 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -6,12 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i*)
 open Pp
-open Errors
-open Util
 open Names
-(*i*)
 
 (*s Pretty-print. *)
 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 296fb2811..f170ff023 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -17,7 +17,7 @@ open Summary
 open Libobject
 open Lib
 open Notation_term
-open Libnames
+open Globnames
 
 type key =
   | RefKey of global_reference
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 6146bc42e..0c39c5d47 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -17,6 +17,7 @@ open Errors
 open Util
 open Names
 open Libnames
+open Globnames
 open Misctypes
 open Syntax_def
 open Notation_term
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index b4e121b4b..eaa4863c6 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -9,6 +9,7 @@
 open Pp
 open Names
 open Libnames
+open Globnames
 open Misctypes
 
 (** [locate_global_with_alias] locates global reference possibly following