- further simplifications (??) of the status dependencies

[helm.git] / matita / matita / matita.ml

diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml
index cefb46e29d1bea322b50d66216cffde1b5c519c5..d84203aa4dcbe0706ff77df40d177eb822ed2403 100644 (file)
--- a/matita/matita/matita.ml
+++ b/matita/matita/matita.ml
@@ -128,7 +128,7 @@ let _ =
     in
     addDebugItem "dump aliases" (fun _ ->
       let status = script#grafite_status in
-      LexiconEngine.dump_aliases prerr_endline "" status);
+      GrafiteDisambiguate.dump_aliases prerr_endline "" status);
 (* FG: DEBUGGING   
     addDebugItem "dump interpretations" (fun _ ->
       let status = script#lexicon_status in