Déplacement de global_reference dans Names pour pouvoir lier Nametab à grammar.cma

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2112 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 17 insertions, 14 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 93e8d4cf50..68ff965b25 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -10,6 +10,7 @@
 
 open Pp
 open Util
+open Names
 open Term
 open Lib
 open Extraction
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 77bea2b8b5..4f380271f5 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -12,7 +12,7 @@
 
 open Miniml
 open Mlutil
-open Term
+open Names
 
 val extract_to_file : 
   string -> extraction_params -> ml_decl list -> global_reference list -> unit
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 173c443566..c358e593d6 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -20,14 +20,15 @@ let destructurate t =
   match Term.kind_of_term c, args with
     | Term.IsConst sp, args ->
 	Kapp (Names.string_of_id
-		(Names.basename (Global.sp_of_global (Term.ConstRef sp))),args)
+		(Names.basename (Global.sp_of_global (Names.ConstRef sp))),
+                args)
     | Term.IsMutConstruct csp , args ->
 	Kapp (Names.string_of_id
-		(Names.basename (Global.sp_of_global (Term.ConstructRef csp))),
-	      args)
+		(Names.basename (Global.sp_of_global(Names.ConstructRef csp))),
+	        args)
     | Term.IsMutInd isp, args ->
 	Kapp (Names.string_of_id
-		(Names.basename (Global.sp_of_global (Term.IndRef isp))),args)
+		(Names.basename (Global.sp_of_global (Names.IndRef isp))),args)
     | Term.IsVar id,[] -> Kvar(Names.string_of_id id)
     | Term.IsProd (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
     | Term.IsProd (Names.Name _,_,_),[] ->
@@ -40,9 +41,9 @@ let dest_const_apply t =
   let f,args = Reduction.whd_stack t in
   let ref = 
   match Term.kind_of_term f with 
-    | Term.IsConst sp         -> Term.ConstRef sp
-    | Term.IsMutConstruct csp -> Term.ConstructRef csp
-    | Term.IsMutInd isp       -> Term.IndRef isp
+    | Term.IsConst sp         -> Names.ConstRef sp
+    | Term.IsMutConstruct csp -> Names.ConstructRef csp
+    | Term.IsMutInd isp       -> Names.IndRef isp
     | _ -> raise Destruct
   in
   Names.basename (Global.sp_of_global ref), args
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index d79e43813d..903a8c0ed4 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -702,20 +702,21 @@ let pp_cmds_of_inner_types inner_types target_uri =
 let print sp fn =
  let module D = Declarations in
  let module G = Global in
- let module N = Nametab in
+ let module N = Names in
+ let module Nt = Nametab in
  let module T = Term in
  let module X = Xml in
-  let (_,id) = N.repr_qualid sp in
+  let (_,id) = Nt.repr_qualid sp in
   let glob_ref = Nametab.locate sp in
   let env = (Safe_typing.env_of_safe_env (G.safe_env ())) in
   reset_ids () ;
   let inner_types = ref [] in
   let sp,tag,pp_cmds =
    match glob_ref with
-      T.VarRef sp ->
+      N.VarRef sp ->
        let (body,typ) = G.lookup_named id in
         sp,Variable,print_variable id body (T.body_of_type typ) env inner_types
-    | T.ConstRef sp ->
+    | N.ConstRef sp ->
        let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
         G.lookup_constant sp in
        let hyps = string_list_of_named_context_list hyps in
@@ -726,12 +727,12 @@ let print sp fn =
             None ->   print_axiom id typ [] hyps env inner_types
           | Some c -> print_definition id c typ [] hyps env inner_types
         end
-    | T.IndRef (sp,_) ->
+    | N.IndRef (sp,_) ->
        let {D.mind_packets=packs ; D.mind_hyps=hyps} = G.lookup_mind sp in
         let hyps = string_list_of_named_context_list hyps in
          sp,Inductive,
           print_mutual_inductive packs [] hyps env inner_types
-    | T.ConstructRef _ ->
+    | N.ConstructRef _ ->
        Util.anomaly ("print: this should not happen")
   in
    Xml.pp pp_cmds fn ;