- de-ALB-ing

- added a debugging item for notation

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 0066d1c1816fcc5d3a7ab8ea142d1eef1744ba4f..b9019a035bf809c0be3871750c5c76cd7ac9f3c3 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -29,9 +29,6 @@ open MatitaGtkMisc
 open MatitaTypes
 open MatitaMisc
 
-(* ALB to link paramodulation... *)
-let _ = Paramodulation.Saturation.init ()
-
 (** {2 Initialization} *)
 
 let _ =
@@ -43,7 +40,8 @@ let _ =
   MatitamakeLib.initialize ();
   CicEnvironment.set_trust (* environment trust *)
     (let trust = Helm_registry.get_bool "matita.environment_trust" in
-     fun _ -> trust)
+     fun _ -> trust);
+  Paramodulation.Saturation.init ()
 
 (** {2 GUI callbacks} *)
 
@@ -149,10 +147,12 @@ let _ =
             (UriManager.name_of_uri u ^ ":"
              ^ UriManager.name_of_uri s ^ " -> " ^ UriManager.name_of_uri t))
         (CoercDb.to_list ()));
+    addDebugItem "print top-level grammar entries"
+      CicNotationParser.print_l2_pattern;
     addDebugItem "rotate light bulbs"
       (fun _ ->
          let nb = gui#main#hintNotebook in
-         nb#goto_page ((nb#current_page + 1) mod 3))
+         nb#goto_page ((nb#current_page + 1) mod 3));
   end
 
   (** </DEBUGGING> *)