X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.ml;h=f8cc4efb44f6806115cf95c4a278b69b1420e666;hb=3bcbcf37670fae4d07baaa91032f49141a860cb0;hp=d63e327f03b89e8d68a58b7ce2a80e68e945ff78;hpb=45a9e84c12f57e5473eccc6f611cdbb343998d5d;p=helm.git

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index d63e327f0..f8cc4efb4 100644
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -67,6 +67,8 @@ let script =
             ~parent:gui#main#toplevel ())
       ()
   in
+  Predefined_virtuals.load_predefined_virtuals ();
+  Predefined_virtuals.load_predefined_classes ();
   gui#sourceView#source_buffer#begin_not_undoable_action ();
   s#reset (); 
   s#template (); 
@@ -118,7 +120,10 @@ let _ =
     in
     addDebugItem "dump aliases" (fun _ ->
       let status = script#lexicon_status in
-      HLog.debug (DisambiguatePp.pp_environment status.LexiconEngine.aliases));
+      HLog.debug (String.concat "\n"
+       (DisambiguateTypes.Environment.fold
+         (fun _ x l -> (LexiconAstPp.pp_alias x)::l)
+         status.LexiconEngine.aliases [])));
     addDebugItem "dump environment to \"env.dump\"" (fun _ ->
       let oc = open_out "env.dump" in
       CicEnvironment.dump_to_channel oc;
@@ -236,9 +241,9 @@ let _ =
 *)
     addDebugSeparator ();
     addDebugItem "enable multiple disambiguation passes (default)"
-      (fun _ -> GrafiteDisambiguator.only_one_pass := false);
+      (fun _ -> MultiPassDisambiguator.only_one_pass := false);
     addDebugItem "enable only one disambiguation pass"
-      (fun _ -> GrafiteDisambiguator.only_one_pass := true);
+      (fun _ -> MultiPassDisambiguator.only_one_pass := true);
     addDebugItem "always show all disambiguation errors"
       (fun _ -> MatitaGui.all_disambiguation_passes := true);
     addDebugItem "prune disambiguation errors"