]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: qualified names were not generated correctly when the dirname was not
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 4 Nov 2007 18:24:57 +0000 (18:24 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 4 Nov 2007 18:24:57 +0000 (18:24 +0000)
empty.

helm/software/matita/matitacLib.ml

index 1da706749fa1194de8e3625dfb91c75c7668d035..c458f2567c414da2903ac7d6930324697549c9a3 100644 (file)
@@ -309,7 +309,7 @@ let main ~mode =
    let f = open_out (basename ^ ".ml") in
     LibrarySync.set_object_declaration_hook
      (fun _ obj ->
-       output_string f (CicExportation.ppobj basename obj);
+       output_string f (CicExportation.ppobj (Filename.basename basename) obj);
        flush f);
   let system_mode =  Helm_registry.get_bool "matita.system" in
   let bench_mode =  Helm_registry.get_bool "matita.bench" in