From 5f015f0329f18ece40772b11db2df2f1de78d251 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 30 Mar 2004 11:10:55 +0000
Subject: 2 choix incorrects

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5610 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/xml/cic2acic.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 70aa0a2916..4877aa3896 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -135,7 +135,9 @@ let token_list_of_kernel_name ~keep_sections 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 N.empty_dirpath
+   | Variable -> 
+       if keep_sections then Lib.cwd () else
+       LN.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) in
    | Constant -> 
        let ref = LN.ConstRef kn in
        if keep_sections then LN.dirpath (Nametab.sp_of_global ref)
@@ -153,9 +155,11 @@ let uri_of_kernel_name ?(keep_sections=false) kn tag =
   let tokens = token_list_of_kernel_name ~keep_sections kn tag in
    "cic:/" ^ String.concat "/" tokens
 
-let uri_of_path dir id tag =
-  let tokens = token_list_of_path dir id tag in
-   "cic:/" ^ String.concat "/" tokens
+let uri_of_declaration id tag =
+ let module LN = Libnames in
+ let dir = LN.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) in
+ let tokens = token_list_of_path dir id tag in
+  "cic:/" ^ String.concat "/" tokens
 
 (* Special functions for handling of CCorn's CProp "sort" *)
 
-- 
cgit v1.2.3