From 57bc566097b92e1f809ae227b674b48ba7953a62 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 4 Nov 2007 18:24:57 +0000 Subject: [PATCH] Bug fixed: qualified names were not generated correctly when the dirname was not empty. --- helm/software/matita/matitacLib.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 1da706749..c458f2567 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/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 -- 2.39.2