*** empty log message ***

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

3 files changed, 10 insertions, 10 deletions

diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index c0bdf07a3e..b3d164122b 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -254,11 +254,11 @@ print_endline "PASSATO" ; flush stdout ;
                 match g with
                    Libnames.ConstructRef ((induri,_),_)
                  | Libnames.IndRef (induri,_) ->
-                    Nametab.sp_of_global None (Libnames.IndRef (induri,0))
+                    Nametab.sp_of_global (Libnames.IndRef (induri,0))
                  | Libnames.VarRef id ->
                     (* Invariant: variables are never cooked in Coq *)
                     raise Not_found
-                 | _ -> Nametab.sp_of_global None g
+                 | _ -> Nametab.sp_of_global g
                in
                Dischargedhypsmap.get_discharged_hyps sp,
                get_module_path_of_section_path sp
diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4
index e2b49a391e..1ee1ef4eab 100644
--- a/contrib/xml/xmlcommand.ml4
+++ b/contrib/xml/xmlcommand.ml4
@@ -420,18 +420,18 @@ let print_term inner_types l env csr =
        >]
 )
    | T.Const kn ->
-       let sp = Nt.sp_of_global None (L.ConstRef kn) in  
+       let sp = Nt.sp_of_global (L.ConstRef kn) in  
 	 X.xml_empty "CONST"
        (add_sort_attribute false
         ["uri",(uri_of_path sp Constant) ; "id", next_id])
    | T.Ind (kn,i) ->
-      let sp = Nt.sp_of_global None (L.IndRef(kn,0)) in  
+      let sp = Nt.sp_of_global (L.IndRef(kn,0)) in  
       X.xml_empty "MUTIND"
        ["uri",(uri_of_path sp Inductive) ;
         "noType",(string_of_int i) ;
         "id", next_id]
    | T.Construct ((kn,i),j) ->
-      let sp = Nt.sp_of_global None (L.IndRef(kn,0)) in  
+      let sp = Nt.sp_of_global (L.IndRef(kn,0)) in  
       X.xml_empty "MUTCONSTRUCT"
        (add_sort_attribute false
         ["uri",(uri_of_path sp Inductive) ;
@@ -439,7 +439,7 @@ let print_term inner_types l env csr =
          "noConstr",(string_of_int j) ;
          "id", next_id])
    | T.Case ({T.ci_ind=(kn,i)},ty,term,a) ->
-      let sp = Nt.sp_of_global None (L.IndRef(kn,0)) in  
+      let sp = Nt.sp_of_global (L.IndRef(kn,0)) in  
       let (uri, typeno) = (uri_of_path sp Inductive),i in
        X.xml_nempty "MUTCASE"
         (add_sort_attribute true
@@ -728,7 +728,7 @@ let print (_,qid as locqid) fn =
        let (_,body,typ) = G.lookup_named id in
         sp,Variable,print_variable id body (T.body_of_type typ) env inner_types
     | Ln.ConstRef kn ->
-       let sp = Nt.sp_of_global None glob_ref in
+       let sp = Nt.sp_of_global glob_ref in
        let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
         G.lookup_constant kn in
        let hyps = string_list_of_named_context_list hyps in
@@ -742,7 +742,7 @@ let print (_,qid as locqid) fn =
 	      print_definition id c typ [] hyps env inner_types
         end
     | Ln.IndRef (kn,_) ->
-       let sp = Nt.sp_of_global None (Ln.IndRef(kn,0)) in  
+       let sp = Nt.sp_of_global (Ln.IndRef(kn,0)) in  
        let {D.mind_packets=packs ;
             D.mind_hyps=hyps;
             D.mind_finite=finite} = G.lookup_mind kn in
diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4
index bcfcbd2ff6..2807a3d6ee 100644
--- a/contrib/xml/xmlentries.ml4
+++ b/contrib/xml/xmlentries.ml4
@@ -50,7 +50,7 @@ END
 let pr_filename = function Some fn -> str " File" ++ str fn | None -> mt ()
 
 let _ = 
-  Pptactic.declare_extra_genarg_pprule 
+  Pptactic.declare_extra_genarg_pprule true
     (rawwit_filename, pr_filename)
     (wit_filename, pr_filename)
 
@@ -76,7 +76,7 @@ open Pp
 let pr_diskname = function Some fn -> str " Disk" ++ str fn | None -> mt ()
 
 let _ = 
-  Pptactic.declare_extra_genarg_pprule 
+  Pptactic.declare_extra_genarg_pprule true
     (rawwit_diskname, pr_diskname)
     (wit_diskname, pr_diskname)