diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-08 16:23:50 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-08 16:23:50 +0000 |
| commit | 1a57a1bcce8bd747548b17303f6681be5a837f37 (patch) | |
| tree | 8bbc3650b8cf505d2b7da3ec06d15a82c9814e70 /contrib | |
| parent | 0b1c4218edbe9c1e43b0b62941905ed2c7d7a848 (diff) | |
nouveau load path
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@828 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 47a800b68..a321ce1ab 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -110,7 +110,8 @@ let uri_of_path sp = match sl with [] -> assert false (*V7 WHAT NOW? *) | module_name::_ -> - trim_wrong_uri_prefix (Library.module_filename module_name) + let _,file = Library.module_filename module_name in + trim_wrong_uri_prefix file in "cic:" ^ module_path ^ "/" ^ (String.concat "/" sl) ^ "/" ^ (N.string_of_id id) ^ "." ^ (ext_of_sp sp) @@ -786,10 +787,10 @@ let printModule id dn = let sp = Lib.make_path id N.OBJ in let ls = L.module_segment (Some str) in print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ " " ^ - L.module_filename str ^ "\n") ; + (snd (L.module_filename str)) ^ "\n") ; print_closed_section str ls dn ; print_if_verbose ("MODULE_END " ^ str ^ " " ^ N.string_of_path sp ^ " " ^ - L.module_filename str ^ "\n") + (snd (L.module_filename str)) ^ "\n") ;; (* printSection identifier directory_name *) |