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

49 files changed, 87 insertions, 64 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 58d809bdb..0f89f348e 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -2,7 +2,7 @@ let contrib_name = "btauto"
 
 let init_constant dir s =
   let find_constant contrib dir s =
-    Libnames.constr_of_global (Coqlib.find_reference contrib dir s)
+    Globnames.constr_of_global (Coqlib.find_reference contrib dir s)
   in
   find_constant contrib_name dir s
 
@@ -10,7 +10,7 @@ let get_constant dir s = lazy (Coqlib.gen_constant contrib_name dir s)
 
 let get_inductive dir s =
   let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in
-  Lazy.lazy_from_fun (fun () -> Libnames.destIndRef (glob_ref ()))
+  Lazy.lazy_from_fun (fun () -> Globnames.destIndRef (glob_ref ()))
 
 let decomp_term (c : Term.constr) =
   Term.kind_of_term (Term.strip_outer_cast c)
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 7c097c6d6..6d3a5be39 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -157,7 +157,7 @@ let special_whd env =
   let infos=Closure.create_clos_infos Closure.betadeltaiota env in
     (fun t -> Closure.whd_val infos (Closure.inject t))
 
-let _eq = Libnames.constr_of_global (Coqlib.glob_eq)
+let _eq = Globnames.constr_of_global (Coqlib.glob_eq)
 
 let decompose_eq env id =
   let typ = Environ.named_type id env in
@@ -247,7 +247,7 @@ let rec glob_of_pat =
 	    add_params (pred n) (GHole(dummy_loc,
 				       Evar_kinds.TomatchTypeParameter(ind,n))::q) in
 	    let args = List.map glob_of_pat lpat in
-	      glob_app(loc,GRef(dummy_loc,Libnames.ConstructRef cstr),
+	      glob_app(loc,GRef(dummy_loc,Globnames.ConstructRef cstr),
 		   add_params mind.Declarations.mind_nparams args)
 
 let prod_one_hyp = function
@@ -334,7 +334,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	     (if expected = 0 then str "none" else int expected) ++ spc () ++
 	     str "expected.") in
   let app_ind =
-    let rind = GRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in
+    let rind = GRef (dummy_loc,Globnames.IndRef pinfo.per_ind) in
     let rparams = List.map detype_ground pinfo.per_params in
     let rparams_rec =
       List.map
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 820da1c3c..2d069b497 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -505,7 +505,7 @@ let instr_cut mkstat _thus _then cut gls0 =
 
 
 (* iterated equality *)
-let _eq = Libnames.constr_of_global (Coqlib.glob_eq)
+let _eq = Globnames.constr_of_global (Coqlib.glob_eq)
 
 let decompose_eq id gls =
   let typ = pf_get_hyp_typ gls id in
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 1b443f753..0f0b902c3 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 02a496bec..a081d74ae 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 aa536b1dc..2c845ce32 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 e587bf212..c846d2d0f 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 d9ee92c05..2533e3a39 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 fe249cd65..a8fb02993 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 a5b57a474..f96447c15 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 f03170948..3221909bc 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 630db6f06..30f1df45d 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 6380ee7ec..bfaecd0f0 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 0565522bf..29a0fb44f 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 d99bca6f4..61759dc24 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 667182480..ecedc9002 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 a3b7124e1..7505664a6 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
 
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 566b2b8b0..7633cc144 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 379aaff18..b3120735c 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 a45d3075f..bc15cb501 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 be69b0675..4ad8aa18f 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 a226cc455..fa2b37e96 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 7d1e57f4a..142a1560b 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 780e3f3e7..269439a53 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 5587e9fbb..8a2406e36 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
 
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 1a629aac9..c9760de17 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -17,6 +17,7 @@ open Tactics
 open Clenv
 open Names
 open Libnames
+open Globnames
 open Tacticals
 open Tacmach
 open Fourier
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index a3bb2eee9..046b65ee8 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -15,6 +15,7 @@ open Tacticals
 open Tactics
 open Indfun_common
 open Libnames
+open Globnames
 open Misctypes
 
 let msgnl = Pp.msgnl
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index b38503cb9..21f77e438 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -101,7 +101,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let env_with_params_and_predicates = List.fold_right Environ.push_named new_predicates env_with_params in
   let rel_as_kn =
     fst (match princ_type_info.indref with
-	   | Some (Libnames.IndRef ind) -> ind
+	   | Some (Globnames.IndRef ind) -> ind
 	   | _ -> error "Not a valid predicate"
 	)
   in
@@ -660,7 +660,7 @@ let build_scheme fas =
 	    let f_as_constant =
 	      try
 		match Nametab.global f with
-		  | Libnames.ConstRef c -> c
+		  | Globnames.ConstRef c -> c
 		  | _ -> Errors.error "Functional Scheme can only be used with functions"
 	      with Not_found ->
 	      	Errors.error ("Cannot find "^ Libnames.string_of_reference f)
@@ -692,7 +692,7 @@ let build_case_scheme fa =
 (*     Constrintern.global_reference  id *)
 (*   in  *)
   let funs =  (fun (_,f,_) ->
-		 try Libnames.constr_of_global (Nametab.global f)
+		 try Globnames.constr_of_global (Nametab.global f)
 		 with Not_found ->
 		   Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
   let first_fun = destConst  funs in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index cf9b54a94..d1fc8ef33 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -5,6 +5,7 @@ open Term
 open Glob_term
 open Glob_ops
 open Libnames
+open Globnames
 open Indfun_common
 open Errors
 open Util
@@ -971,7 +972,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    in
 		    mkGProd(n,t,new_b),id_to_exclude
 		  with Continue ->
-		    let jmeq = Libnames.IndRef (destInd (jmeq ())) in
+		    let jmeq = Globnames.IndRef (destInd (jmeq ())) in
 		    let ty' = Pretyping.understand Evd.empty env ty in
 		    let ind,args' = Inductive.find_inductive env ty' in
 		    let mib,_ = Global.lookup_inductive ind in
@@ -981,7 +982,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    in
 		    let rt_typ =
 		       GApp(Pp.dummy_loc,
-			    GRef (Pp.dummy_loc,Libnames.IndRef ind),
+			    GRef (Pp.dummy_loc,Globnames.IndRef ind),
 			    (List.map
 			      (fun p -> Detyping.detype false []
 				 (Termops.names_of_rel_context env)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 6433fe37c..8967a3ec8 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -441,7 +441,7 @@ let rec pattern_to_term  = function
       let patl_as_term =
 	List.map pattern_to_term patternl
       in
-      mkGApp(mkGRef(Libnames.ConstructRef constr),
+      mkGApp(mkGRef(Globnames.ConstructRef constr),
 	     implicit_args@patl_as_term
 	    )
 
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 761337b07..437ba225d 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -17,7 +17,7 @@ val pattern_to_term : cases_pattern -> glob_constr
    Some basic functions to rebuild glob_constr
    In each of them the location is Util.dummy_loc
 *)
-val mkGRef : Libnames.global_reference -> glob_constr
+val mkGRef : Globnames.global_reference -> glob_constr
 val mkGVar : Names.identifier -> glob_constr
 val mkGApp  : glob_constr*(glob_constr list) -> glob_constr
 val mkGLambda : Names.name * glob_constr * glob_constr -> glob_constr
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d3f56341f..2a6a7dea3 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -5,6 +5,7 @@ open Term
 open Pp
 open Indfun_common
 open Libnames
+open Globnames
 open Glob_term
 open Declarations
 open Misctypes
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index c0b72f0b3..654d42ee1 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -23,4 +23,4 @@ val functional_induction :
   Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
 
 
-val make_graph :  Libnames.global_reference -> unit
+val make_graph :  Globnames.global_reference -> unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index de7e17957..026b9ad0e 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -1,6 +1,7 @@
 open Names
 open Pp
 open Libnames
+open Globnames
 open Refiner
 open Hiddentac 
 let mk_prefix pre id = id_of_string (pre^(string_of_id id))
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index bb59a5c9c..8f80c072c 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -117,9 +117,9 @@ val h_intros: Names.identifier list -> Proof_type.tactic
 val h_id :  Names.identifier
 val hrec_id :  Names.identifier
 val acc_inv_id :  Term.constr Util.delayed
-val ltof_ref : Libnames.global_reference Util.delayed
+val ltof_ref : Globnames.global_reference Util.delayed
 val well_founded_ltof : Term.constr Util.delayed
 val acc_rel : Term.constr Util.delayed
 val well_founded : Term.constr Util.delayed
-val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference 
+val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference
 val list_rewrite : bool -> (Term.constr*bool) list -> Proof_type.tactic
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 4d072eca5..b0897c61e 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -13,6 +13,7 @@ open Names
 open Term
 open Pp
 open Libnames
+open Globnames
 open Tacticals
 open Tactics
 open Indfun_common
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ebe5cebd2..af7506103 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -9,6 +9,7 @@
 (* Merging of induction principles. *)
 
 open Libnames
+open Globnames
 open Tactics
 open Indfun_common
 open Errors
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 0b61c5f85..2005a90e3 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -16,6 +16,7 @@ open Entries
 open Pp
 open Names
 open Libnames
+open Globnames
 open Nameops
 open Errors
 open Util
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 2c82bab7b..ddaf82a18 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -32,6 +32,7 @@ open Tactics
 open Clenv
 open Logic
 open Libnames
+open Globnames
 open Nametab
 open Contradiction
 open Misctypes
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 4bf08912a..ab6ee1573 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -15,6 +15,7 @@ open Flags
 open Term
 open Names
 open Libnames
+open Globnames
 open Nameops
 open Reductionops
 open Tacticals
@@ -744,7 +745,7 @@ let constants_to_unfold =
   let transform s =
     let sp = path_of_string s in
     let dir, id = repr_path sp in
-      Libnames.encode_con dir id
+      Globnames.encode_con dir id
   in
   List.map transform
     [ "Coq.ring.Ring_normalize.interp_cs";
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 298b24850..c1cea8aac 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -31,11 +31,11 @@ let destructurate t =
   let c, args = Term.decompose_app t in
   match Term.kind_of_term c, args with
     | Term.Const sp, args ->
-	Kapp (string_of_global (Libnames.ConstRef sp), args)
+	Kapp (string_of_global (Globnames.ConstRef sp), args)
     | Term.Construct csp , args ->
-	Kapp (string_of_global (Libnames.ConstructRef csp), args)
+	Kapp (string_of_global (Globnames.ConstructRef csp), args)
     | Term.Ind isp, args ->
-	Kapp (string_of_global (Libnames.IndRef isp), args)
+	Kapp (string_of_global (Globnames.IndRef isp), args)
     | Term.Var id,[] -> Kvar(Names.string_of_id id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
     | Term.Prod (Names.Name _,_,_),[] ->
@@ -48,9 +48,9 @@ let dest_const_apply t =
   let f,args = Term.decompose_app t in
   let ref =
   match Term.kind_of_term f with
-    | Term.Const sp      -> Libnames.ConstRef sp
-    | Term.Construct csp -> Libnames.ConstructRef csp
-    | Term.Ind isp       -> Libnames.IndRef isp
+    | Term.Const sp      -> Globnames.ConstRef sp
+    | Term.Construct csp -> Globnames.ConstructRef csp
+    | Term.Ind isp       -> Globnames.IndRef isp
     | _ -> raise Destruct
   in  Nametab.basename_of_global ref, args
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 590776760..c2815aafa 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -16,6 +16,7 @@ open Term
 open Closure
 open Environ
 open Libnames
+open Globnames
 open Tactics
 open Glob_term
 open Tacticals
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index cf51af134..b2e2e5b19 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -14,13 +14,14 @@ open Pcoq
 open Glob_term
 open Topconstr
 open Libnames
+open Globnames
 open Coqlib
 open Bigint
 
 exception Non_closed_ascii
 
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
-let make_kn dir id = Libnames.encode_mind (make_dir dir) (id_of_string id)
+let make_kn dir id = Globnames.encode_mind (make_dir dir) (id_of_string id)
 let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
 
 let ascii_module = ["Coq";"Strings";"Ascii"]
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 984bae418..b67cbb934 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -10,6 +10,7 @@
 
 open Bigint
 open Libnames
+open Globnames
 open Glob_term
 
 (*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index b3195f281..f8161c52f 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -13,6 +13,7 @@ open Names
 open Pcoq
 open Topconstr
 open Libnames
+open Globnames
 
 exception Non_closed_number
 
@@ -31,7 +32,7 @@ let make_path dir id = Libnames.make_path dir (id_of_string id)
 let r_path = make_path rdefinitions "R"
 
 (* TODO: temporary hack *)
-let make_path dir id = Libnames.encode_con dir (id_of_string id)
+let make_path dir id = Globnames.encode_con dir (id_of_string id)
 
 let r_kn = make_path rdefinitions "R"
 let glob_R = ConstRef r_kn
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 640806d87..ac17492d2 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Pcoq
 open Libnames
+open Globnames
 open Topconstr
 open Ascii_syntax
 open Glob_term
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 450d57969..a69ec9ed1 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -22,6 +22,7 @@ exception Non_closed_number
 (**********************************************************************)
 
 open Libnames
+open Globnames
 open Glob_term
 
 let binnums = ["Coq";"Numbers";"BinNums"]
@@ -32,7 +33,7 @@ let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
 let positive_path = make_path binnums "positive"
 
 (* TODO: temporary hack *)
-let make_kn dir id = Libnames.encode_mind dir id
+let make_kn dir id = Globnames.encode_mind dir id
 
 let positive_kn = make_kn (make_dir binnums) (id_of_string "positive")
 let glob_positive = IndRef (positive_kn,0)
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 78a402898..ec0910d7f 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -125,16 +125,16 @@ let token_list_of_path dir id tag =
 
 let token_list_of_kernel_name tag =
  let module N = Names in
- let module LN = Libnames in
+ let module GN = Globnames in
  let id,dir = match tag with
    | Variable kn ->
        N.id_of_label (N.label kn), Lib.cwd ()
    | Constant con ->
        N.id_of_label (N.con_label con),
-       Lib.remove_section_part (LN.ConstRef con)
+       Lib.remove_section_part (GN.ConstRef con)
    | Inductive kn ->
        N.id_of_label (N.mind_label kn),
-       Lib.remove_section_part (LN.IndRef (kn,0))
+       Lib.remove_section_part (GN.IndRef (kn,0))
  in
  token_list_of_path dir id (etag_of_tag tag)
 ;;
@@ -431,13 +431,13 @@ print_endline "PASSATO" ; flush stdout ;
           let subst,residual_args,uninst_vars =
            let variables,basedir =
              try
-               let g = Libnames.global_of_constr h in
+               let g = Globnames.global_of_constr h in
                let sp =
                 match g with
-                   Libnames.ConstructRef ((induri,_),_)
-                 | Libnames.IndRef (induri,_) ->
-                    Nametab.path_of_global (Libnames.IndRef (induri,0))
-                 | Libnames.VarRef id ->
+                   Globnames.ConstructRef ((induri,_),_)
+                 | Globnames.IndRef (induri,_) ->
+                    Nametab.path_of_global (Globnames.IndRef (induri,0))
+                 | Globnames.VarRef id ->
                     (* Invariant: variables are never cooked in Coq *)
                     raise Not_found
                  | _ -> Nametab.path_of_global g
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 93ff00dff..81dba546e 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -470,15 +470,15 @@ let kind_of_constant kn =
 ;;
 
 let kind_of_global r =
-  let module Ln = Libnames in
+  let module Gn = Globnames in
   match r with
-  | Ln.IndRef kn | Ln.ConstructRef (kn,_) ->
+  | Gn.IndRef kn | Gn.ConstructRef (kn,_) ->
       let isrecord =
 	try let _ = Recordops.lookup_projections kn in Declare.KernelSilent
         with Not_found -> Declare.KernelVerbose in
       kind_of_inductive isrecord (fst kn)
-  | Ln.VarRef id -> kind_of_variable id
-  | Ln.ConstRef kn -> kind_of_constant kn
+  | Gn.VarRef id -> kind_of_variable id
+  | Gn.ConstRef kn -> kind_of_constant kn
 ;;
 
 let print_object_kind uri (xmltag,variation) =
@@ -504,12 +504,12 @@ let print internal glob_ref kind xml_library_root =
  let module Nt = Nametab in
  let module T = Term in
  let module X = Xml in
- let module Ln = Libnames in
+ let module Gn = Globnames in
   (* Variables are the identifiers of the variables in scope *)
   let variables = search_variables () in
   let tag,obj =
    match glob_ref with
-      Ln.VarRef id ->
+      Gn.VarRef id ->
        (* this kn is fake since it is not provided by Coq *)
        let kn =
         let (mod_path,dir_path) = Lib.current_prefix () in
@@ -517,7 +517,7 @@ let print internal glob_ref kind xml_library_root =
        in
        let (_,body,typ) = G.lookup_named id in
         Cic2acic.Variable kn,mk_variable_obj id body typ
-    | Ln.ConstRef kn ->
+    | Gn.ConstRef kn ->
        let id = N.id_of_label (N.con_label kn) in
        let cb = G.lookup_constant kn in
        let val0 = D.body_of_constant cb in
@@ -525,14 +525,14 @@ let print internal glob_ref kind xml_library_root =
        let hyps = cb.D.const_hyps in
        let typ = Typeops.type_of_constant_type (Global.env()) typ in
         Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
-    | Ln.IndRef (kn,_) ->
+    | Gn.IndRef (kn,_) ->
        let mib = G.lookup_mind kn in
        let {D.mind_nparams=nparams;
 	    D.mind_packets=packs ;
             D.mind_hyps=hyps;
             D.mind_finite=finite} = mib in
           Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite
-    | Ln.ConstructRef _ ->
+    | Gn.ConstructRef _ ->
        Errors.error ("a single constructor cannot be printed in XML")
   in
   let fn = filename_of_path xml_library_root tag in
@@ -580,7 +580,7 @@ let _ =
   Declare.set_xml_declare_variable
    (function (sp,kn) ->
      let id = Libnames.basename sp in
-     print Declare.UserVerbose (Libnames.VarRef id) (kind_of_variable id) xml_library_root ;
+     print Declare.UserVerbose (Globnames.VarRef id) (kind_of_variable id) xml_library_root ;
      proof_to_export := None)
 ;;
 
@@ -589,7 +589,7 @@ let _ =
    (function (internal,kn) ->
      match !proof_to_export with
         None ->
-          print internal (Libnames.ConstRef kn) (kind_of_constant kn)
+          print internal (Globnames.ConstRef kn) (kind_of_constant kn)
 	    xml_library_root
       | Some pftreestate ->
          (* It is a proof. Let's export it starting from the proof-tree *)
@@ -603,7 +603,7 @@ let _ =
 let _ =
   Declare.set_xml_declare_inductive
    (function (isrecord,(sp,kn)) ->
-      print Declare.UserVerbose (Libnames.IndRef (Names.mind_of_kn kn,0))
+      print Declare.UserVerbose (Globnames.IndRef (Names.mind_of_kn kn,0))
         (kind_of_inductive isrecord (Names.mind_of_kn kn))
         xml_library_root)
 ;;