~keep_sections was now redundant. Got rid of.

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

2 files changed, 16 insertions, 19 deletions

diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 4a7c3823d..22e9670d5 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -95,6 +95,7 @@ let subtract l1 l2 =
    Names.make_dirpath (List.rev (aux l1'))
 ;;
 
+(*CSC: Dead code to be removed
 let token_list_of_kernel_name ~keep_sections kn tag =
  let module N = Names in
   let (modpath,dirpath,label) = Names.repr_kn kn in
@@ -124,6 +125,7 @@ let token_list_of_kernel_name ~keep_sections kn tag =
     (if keep_sections then token_list_of_dirpath dirpath else []) @
     [N.string_of_label label ^ "." ^ (ext_of_tag tag)]
 ;;
+*)
 
 let token_list_of_path dir id tag =
  let module N = Names in
@@ -131,28 +133,23 @@ let token_list_of_path dir id tag =
    List.rev_map N.string_of_id (N.repr_dirpath dirpath) in
   token_list_of_dirpath dir @ [N.string_of_id id ^ "." ^ (ext_of_tag tag)]
 
-let token_list_of_kernel_name ~keep_sections kn tag =
+let token_list_of_kernel_name kn tag =
  let module N = Names in
  let module LN = Libnames in
  let dir = match tag with
    | Variable -> 
-       if keep_sections then Lib.cwd () else
-       LN.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
+       Lib.cwd ()
    | Constant -> 
-       let ref = LN.ConstRef kn in
-       if keep_sections then LN.dirpath (Nametab.sp_of_global ref)
-       else Lib.library_part ref
+       Lib.library_part (LN.ConstRef kn)
    | Inductive ->
-       let ref = LN.IndRef (kn,0) in
-      if keep_sections then LN.dirpath(Nametab.sp_of_global ref)
-      else Lib.library_part ref
+       Lib.library_part (LN.IndRef (kn,0))
  in
  let id = N.id_of_label (N.label kn) in
  token_list_of_path dir id tag
 ;;
 
-let uri_of_kernel_name ?(keep_sections=false) kn tag =
-  let tokens = token_list_of_kernel_name ~keep_sections kn tag in
+let uri_of_kernel_name kn tag =
+  let tokens = token_list_of_kernel_name kn tag in
    "cic:/" ^ String.concat "/" tokens
 
 let uri_of_declaration id tag =
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 5743a0bf2..a6d744ba4 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -182,12 +182,12 @@ let rec join_dirs cwd =
       join_dirs newcwd tail
 ;;
 
-let filename_of_path ?(keep_sections=false) xml_library_root kn tag =
+let filename_of_path xml_library_root kn tag =
  let module N = Names in
   match xml_library_root with
      None -> None  (* stdout *)
    | Some xml_library_root' ->
-      let tokens = Cic2acic.token_list_of_kernel_name ~keep_sections kn tag in
+      let tokens = Cic2acic.token_list_of_kernel_name kn tag in
        Some (join_dirs xml_library_root' tokens)
 ;;
 
@@ -512,7 +512,7 @@ let print internal glob_ref kind xml_library_root =
  let module Ln = Libnames in
   (* Variables are the identifiers of the variables in scope *)
   let variables = search_variables () in
-  let keep_sections,kn,tag,obj =
+  let kn,tag,obj =
    match glob_ref with
       Ln.VarRef id ->
        let sp = Declare.find_section_variable id in
@@ -522,23 +522,23 @@ let print internal glob_ref kind xml_library_root =
         N.make_kn mod_path dir_path (N.label_of_id (Ln.basename sp))
        in
        let (_,body,typ) = G.lookup_named id in
-        true,kn,Cic2acic.Variable,mk_variable_obj id body typ
+        kn,Cic2acic.Variable,mk_variable_obj id body typ
     | Ln.ConstRef kn ->
        let id = N.id_of_label (N.label kn) in
        let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
         G.lookup_constant kn in
-        false,kn,Cic2acic.Constant,mk_constant_obj id val0 typ variables hyps
+        kn,Cic2acic.Constant,mk_constant_obj id val0 typ variables hyps
     | Ln.IndRef (kn,_) ->
        let {D.mind_packets=packs ;
             D.mind_hyps=hyps;
             D.mind_finite=finite} = G.lookup_mind kn in
-          false,kn,Cic2acic.Inductive,
+          kn,Cic2acic.Inductive,
            mk_inductive_obj kn packs variables hyps finite
     | Ln.ConstructRef _ ->
        Util.anomaly ("print: this should not happen")
   in
-  let fn = filename_of_path ~keep_sections xml_library_root kn tag in
-  let uri = Cic2acic.uri_of_kernel_name ~keep_sections kn tag in
+  let fn = filename_of_path xml_library_root kn tag in
+  let uri = Cic2acic.uri_of_kernel_name kn tag in
    if not internal then print_object_kind uri kind;
    print_object uri obj Evd.empty None fn
 ;;