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

24 files changed, 27 insertions, 20 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 54ffcd653..43483d2da 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -8,7 +8,7 @@
 
 (*i*)
 open Names
-open Libnames
+open Globnames
 open Decl_kinds
 open Term
 open Sign
diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli
index a484ecf7f..243bb6b7e 100644
--- a/pretyping/arguments_renaming.mli
+++ b/pretyping/arguments_renaming.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Libnames
+open Globnames
 open Environ
 open Term
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 3be7e7862..cc664f9b5 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -12,6 +12,7 @@ open Pp
 open Flags
 open Names
 open Libnames
+open Globnames
 open Nametab
 open Environ
 open Libobject
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 66bb5c6c6..dd5214b04 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -29,7 +29,7 @@ type cl_info_typ = {
   cl_param : int }
 
 (** This is the type of coercion kinds *)
-type coe_typ = Libnames.global_reference
+type coe_typ = Globnames.global_reference
 
 (** This is the type of infos for declared coercions *)
 type coe_info_typ
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c1e0d123d..ab4388047 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -23,6 +23,7 @@ open Nameops
 open Termops
 open Namegen
 open Libnames
+open Globnames
 open Nametab
 open Evd
 open Mod_subst
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e49f2b4eb..3fb679067 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -18,7 +18,7 @@ open Termops
 open Environ
 open Recordops
 open Evarutil
-open Libnames
+open Globnames
 open Evd
 
 type flex_kind_of_term =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5164385ce..0197af56c 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -16,6 +16,7 @@ open Termops
 open Sign
 open Environ
 open Libnames
+open Globnames
 open Mod_subst
 
 (* The kinds of existential variables are now defined in [Evar_kinds] *)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 7a48ee9de..b592d7829 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -12,7 +12,7 @@ open Util
 open Names
 open Sign
 open Term
-open Libnames
+open Globnames
 open Nametab
 open Decl_kinds
 open Misctypes
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index f08b7493c..e9d6a3c29 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -15,6 +15,7 @@ open Errors
 open Util
 open Names
 open Libnames
+open Globnames
 open Nameops
 open Term
 open Namegen
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 554face37..0dfb18d84 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -11,7 +11,7 @@ open Pp
 open Errors
 open Util
 open Names
-open Libnames
+open Globnames
 open Nameops
 open Termops
 open Reductionops
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 9a1425716..f25e6be92 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -19,6 +19,7 @@ open Term
 open Nametab
 open Nameops
 open Libnames
+open Globnames
 open Environ
 open Termops
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 244d03021..1e73e2634 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -9,7 +9,7 @@
 open Errors
 open Util
 open Names
-open Libnames
+open Globnames
 open Nameops
 open Term
 open Glob_term
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 74e5a81ae..c523ce0b2 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -11,7 +11,7 @@ open Names
 open Sign
 open Term
 open Environ
-open Libnames
+open Globnames
 open Nametab
 open Glob_term
 open Mod_subst
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b241336e7..4eeb50cd0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -35,6 +35,7 @@ open Environ
 open Type_errors
 open Typeops
 open Libnames
+open Globnames
 open Nameops
 open Classops
 open List
diff --git a/pretyping/program.ml b/pretyping/program.ml
index bb0cbe1c7..046379ed6 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -33,7 +33,7 @@ let find_reference locstr dir s =
   with Not_found -> anomaly (locstr^": cannot find "^(Libnames.string_of_path sp))
 
 let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
-let coq_constant locstr dir s = Libnames.constr_of_global (coq_reference locstr dir s)
+let coq_constant locstr dir s = Globnames.constr_of_global (coq_reference locstr dir s)
 
 let init_constant dir s () = coq_constant "Program" dir s
 let init_reference dir s () = coq_reference "Program" dir s
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e35004ef1..e2b03d0f2 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -17,7 +17,7 @@ open Errors
 open Util
 open Pp
 open Names
-open Libnames
+open Globnames
 open Nametab
 open Term
 open Typeops
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 6165fac26..0419ae907 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -9,7 +9,7 @@
 open Names
 open Nametab
 open Term
-open Libnames
+open Globnames
 open Libobject
 open Library
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 05136d25d..5505a39d3 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -13,6 +13,7 @@ open Names
 open Nameops
 open Term
 open Libnames
+open Globnames
 open Termops
 open Namegen
 open Declarations
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index c9b139ac9..37531af21 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -15,7 +15,7 @@ open Closure
 open Glob_term
 open Termops
 open Pattern
-open Libnames
+open Globnames
 open Locus
 
 type reduction_tactic_error =
@@ -29,13 +29,13 @@ exception ReductionTacticError of reduction_tactic_error
 
 val is_evaluable : Environ.env -> evaluable_global_reference -> bool
 
-val error_not_evaluable : Libnames.global_reference -> 'a
+val error_not_evaluable : Globnames.global_reference -> 'a
 
 val evaluable_of_global_reference :
-  Environ.env -> Libnames.global_reference -> evaluable_global_reference
+  Environ.env -> Globnames.global_reference -> evaluable_global_reference
 
 val global_of_evaluable_reference :
-  evaluable_global_reference -> Libnames.global_reference
+  evaluable_global_reference -> Globnames.global_reference
 
 exception Redelimination
 
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 2bf15d2f3..c5ce0f45e 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -12,7 +12,7 @@ open Util
 open Term
 open Sign
 open Names
-open Libnames
+open Globnames
 open Mod_subst
 open Pp (* debug *)
 (*i*)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 6be28ebcb..d76fdc85d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -8,7 +8,7 @@
 
 (*i*)
 open Names
-open Libnames
+open Globnames
 open Decl_kinds
 open Term
 open Sign
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 7e283e56d..6c97516ca 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Libnames
+open Globnames
 open Decl_kinds
 open Term
 open Sign
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index a5ba7e98a..fee55e72a 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -19,7 +19,7 @@ open Constrexpr
 open Compat
 open Pp
 open Util
-open Libnames
+open Globnames
 (*i*)
 
 type contexts = Parameters | Properties
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 45857df40..925222766 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -17,7 +17,7 @@ open Mod_subst
 open Constrexpr
 open Errors
 open Pp
-open Libnames
+open Globnames
 
 type contexts = Parameters | Properties