diff options
| author | herbelin | 2004-03-30 11:10:55 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-30 11:10:55 +0000 |
| commit | 5f015f0329f18ece40772b11db2df2f1de78d251 (patch) | |
| tree | 7826718da643a3eda51c1ba27f7af1303a8abfb9 | |
| parent | f5e8da3bbf50e7a826398a05ba7c5cfafe667a6e (diff) | |
2 choix incorrects
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5610 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/xml/cic2acic.ml | 12 |
1 files 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" *) |