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

16 files changed, 18 insertions, 14 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 158221d79..6146998cb 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -35,6 +35,7 @@ open Tacticals
 open Clenv
 open Hiddentac
 open Libnames
+open Globnames
 open Nametab
 open Smartlocate
 open Libobject
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 0dfcb0b68..e34141446 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -17,7 +17,7 @@ open Clenv
 open Pattern
 open Environ
 open Evd
-open Libnames
+open Globnames
 open Vernacexpr
 open Mod_subst
 open Misctypes
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index c13136b95..18ff0a509 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -10,7 +10,7 @@ open Term
 open Names
 open Termdn
 open Pattern
-open Libnames
+open Globnames
 
 (* Discrimination nets with bounded depth.
    See the module dn.ml for further explanations.
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index bfebf7810..a749ba8ab 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -35,7 +35,7 @@ open Classes
 open Topconstr
 open Pfedit
 open Command
-open Libnames
+open Globnames
 open Evd
 open Compat
 open Locus
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index fe380db7c..0d16e4931 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -76,7 +76,7 @@ let my_it_mkLambda_or_LetIn_name s c =
 
 let get_coq_eq () =
   try
-    let eq = Libnames.destIndRef Coqlib.glob_eq in
+    let eq = Globnames.destIndRef Coqlib.glob_eq in
     let _ = Global.lookup_inductive eq in
     (* Do not force the lazy if they are not defined *)
     mkInd eq, Coqlib.build_coq_eq_refl ()
diff --git a/tactics/equality.ml b/tactics/equality.ml
index cfbb30a74..81457fc9c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -19,6 +19,7 @@ open Inductive
 open Inductiveops
 open Environ
 open Libnames
+open Globnames
 open Reductionops
 open Typeops
 open Typing
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 4f1174916..5abbe7ae9 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -236,7 +236,7 @@ let coq_refl_leibniz1_pattern = PATTERN [ forall x:_, _ x x ]
 let coq_refl_leibniz2_pattern = PATTERN [ forall A:_, forall x:A, _ A x x ]
 let coq_refl_jm_pattern       = PATTERN [ forall A:_, forall x:A, _ A x A x ]
 
-open Libnames
+open Globnames
 
 let match_with_equation t =
   if not (isApp t) then raise NoEquationFound;
@@ -489,7 +489,7 @@ let match_eqdec t =
         false,op_or,matches (Lazy.force coq_eqdec_rev_pattern) t in
   match subst with
   | [(_,typ);(_,c1);(_,c2)] ->
-      eqonleft, Libnames.constr_of_global (Lazy.force op), c1, c2, typ
+      eqonleft, Globnames.constr_of_global (Lazy.force op), c1, c2, typ
   | _ -> anomaly "Unexpected pattern"
 
 (* Patterns "~ ?" and "? -> False" *)
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index dce518f87..9522a75d9 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -13,7 +13,7 @@ open Term
 open Libobject
 open Library
 open Pattern
-open Libnames
+open Globnames
 
 (* Named, bounded-depth, term-discrimination nets.
    Implementation:
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 652ff4f42..9ddb05cd2 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -8,7 +8,7 @@
 
 open Term
 open Pattern
-open Libnames
+open Globnames
 
 (** Named, bounded-depth, term-discrimination nets. *)
 module Make :
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 75f6bdb7c..004599f45 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -37,6 +37,7 @@ open Constrexpr
 open Pfedit
 open Command
 open Libnames
+open Globnames
 open Evd
 open Compat
 open Misctypes
@@ -1736,7 +1737,7 @@ let add_morphism_infer glob m n =
 	  (fun () ->
 	    Lemmas.start_proof instance_id kind instance
 	      (fun _ -> function
-		Libnames.ConstRef cst ->
+		Globnames.ConstRef cst ->
 		  add_instance (Typeclasses.new_instance (Lazy.force proper_class) None
 				   glob (ConstRef cst));
 		  declare_projection n instance_id (ConstRef cst)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a0fd61c06..d98167ed0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -26,6 +26,7 @@ open Util
 open Names
 open Nameops
 open Libnames
+open Globnames
 open Nametab
 open Smartlocate
 open Pfedit
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 75f0b4a51..bf9353076 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -21,7 +21,7 @@ open Inductive
 open Inductiveops
 open Reductionops
 open Environ
-open Libnames
+open Globnames
 open Evd
 open Pfedit
 open Tacred
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 5cf460366..7294a319d 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -20,7 +20,7 @@ open Evar_refiner
 open Clenv
 open Redexpr
 open Tacticals
-open Libnames
+open Globnames
 open Genarg
 open Tacexpr
 open Nametab
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 570c6c7a1..79c1797e4 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -11,7 +11,7 @@
 open Term
 open Hipattern
 open Names
-open Libnames
+open Globnames
 open Pp
 open Proof_type
 open Tacticals
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 0e7009113..ce7ac29f1 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -14,7 +14,7 @@ open Term
 open Pattern
 open Patternops
 open Glob_term
-open Libnames
+open Globnames
 open Nametab
 
 (* Discrimination nets of terms.
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index c4e747be0..b325a7950 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -8,7 +8,7 @@
 
 open Term
 open Pattern
-open Libnames
+open Globnames
 open Names
 
 (** Discrimination nets of terms. *)