From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 4 Nov 2007 18:24:57 +0000 (+0000)
Subject: Bug fixed: qualified names were not generated correctly when the dirname was not
X-Git-Tag: 0.4.95@7852~61
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=27d1c17647fd6d8ec4749160f921c404da0028e3

Bug fixed: qualified names were not generated correctly when the dirname was not
empty.
---

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index 1da706749..c458f2567 100644
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -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