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

8 files changed, 11 insertions, 11 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 566b2b8b08..7633cc1448 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -15,7 +15,7 @@ open Tacmach
 open Errors
 open Util
 open Declarations
-open Libnames
+open Globnames
 open Inductiveops
 
 let qflag=ref true
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 379aaff18a..b3120735ce 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -8,7 +8,7 @@
 
 open Term
 open Names
-open Libnames
+open Globnames
 
 val qflag : bool ref
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a45d3075fa..bc15cb5015 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -24,7 +24,7 @@ open Declarations
 open Formula
 open Sequent
 open Names
-open Libnames
+open Globnames
 open Misctypes
 
 let compare_instance inst1 inst2=
@@ -40,11 +40,11 @@ let compare_gr id1 id2 =
   if id1==id2 then 0 else
     if id1==dummy_id then 1
     else if id2==dummy_id then -1
-    else Libnames.RefOrdered.compare id1 id2
+    else Globnames.RefOrdered.compare id1 id2
 
 module OrderedInstance=
 struct
-  type t=instance * Libnames.global_reference
+  type t=instance * Globnames.global_reference
   let compare (inst1,id1) (inst2,id2)=
     (compare_instance =? compare_gr) inst2 inst1 id2 id1
     (* we want a __decreasing__ total order *)
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index be69b06758..4ad8aa18fe 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -9,7 +9,7 @@
 open Term
 open Tacmach
 open Names
-open Libnames
+open Globnames
 open Rules
 
 val collect_quantified : Sequent.t -> Formula.t list * Sequent.t
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index a226cc4555..fa2b37e966 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -17,7 +17,7 @@ open Termops
 open Declarations
 open Formula
 open Sequent
-open Libnames
+open Globnames
 open Locus
 
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 7d1e57f4a8..142a1560b5 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -9,7 +9,7 @@
 open Term
 open Tacmach
 open Names
-open Libnames
+open Globnames
 
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 780e3f3e7e..269439a535 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -13,7 +13,7 @@ open Formula
 open Unify
 open Tacmach
 open Names
-open Libnames
+open Globnames
 open Pp
 
 let newcnt ()=
@@ -70,7 +70,7 @@ module Hitem=
 struct
   type t = h_item
   let compare (id1,co1) (id2,co2)=
-    (Libnames.RefOrdered.compare
+    (Globnames.RefOrdered.compare
      =? (fun oc1 oc2 ->
 	   match oc1,oc2 with
 	       Some (m1,c1),Some (m2,c2) ->
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 5587e9fbb5..8a2406e364 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -12,7 +12,7 @@ open Util
 open Formula
 open Tacmach
 open Names
-open Libnames
+open Globnames
 
 module OrderedConstr: Set.OrderedType with type t=constr