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

2 files changed, 20 insertions, 20 deletions

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)
 ;;