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

14 files changed, 14 insertions, 7 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 1b443f7535..0f0b902c34 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -15,6 +15,7 @@ open Declarations
 open Namegen
 open Nameops
 open Libnames
+open Globnames
 open Table
 open Miniml
 open Mlutil
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 02a496bec1..a081d74ae0 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Libnames
+open Globnames
 open Miniml
 open Mlutil
 open Pp
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index aa536b1dce..2c845ce324 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -10,6 +10,7 @@ open Term
 open Declarations
 open Names
 open Libnames
+open Globnames
 open Pp
 open Errors
 open Util
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index e587bf2120..c846d2d0f3 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -10,6 +10,7 @@
 
 open Names
 open Libnames
+open Globnames
 
 val simple_extraction : reference -> unit
 val full_extraction : string option -> reference list -> unit
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index d9ee92c05e..2533e3a39f 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -21,7 +21,7 @@ open Inductiveops
 open Recordops
 open Namegen
 open Summary
-open Libnames
+open Globnames
 open Nametab
 open Miniml
 open Table
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index fe249cd65c..a8fb02993e 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -14,6 +14,7 @@ open Util
 open Names
 open Nameops
 open Libnames
+open Globnames
 open Table
 open Miniml
 open Mlutil
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index a5b57a4742..f96447c156 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -12,7 +12,7 @@ open Pp
 open Errors
 open Util
 open Names
-open Libnames
+open Globnames
 
 (* The [signature] type is used to know how many arguments a CIC
    object expects, and what these arguments will become in the ML
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index f031709488..3221909bce 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -12,6 +12,7 @@ open Errors
 open Util
 open Names
 open Libnames
+open Globnames
 open Nametab
 open Table
 open Miniml
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 630db6f069..30f1df45dd 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -10,7 +10,7 @@ open Errors
 open Util
 open Names
 open Term
-open Libnames
+open Globnames
 open Miniml
 open Table
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 6380ee7ecb..bfaecd0f06 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -9,7 +9,7 @@
 open Names
 open Declarations
 open Environ
-open Libnames
+open Globnames
 open Errors
 open Util
 open Miniml
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index 0565522bf5..29a0fb44f7 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -9,7 +9,7 @@
 open Names
 open Declarations
 open Environ
-open Libnames
+open Globnames
 open Miniml
 open Mod_subst
 
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index d99bca6f4c..61759dc240 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -13,7 +13,7 @@ open Errors
 open Util
 open Names
 open Nameops
-open Libnames
+open Globnames
 open Table
 open Miniml
 open Mlutil
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 6671824807..ecedc9002d 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -15,6 +15,7 @@ open Summary
 open Libobject
 open Goptions
 open Libnames
+open Globnames
 open Errors
 open Util
 open Pp
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index a3b7124e1d..7505664a60 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Libnames
+open Globnames
 open Miniml
 open Declarations