From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 12 Sep 2005 16:36:27 +0000 (+0000)
Subject: - de-ALB-ing
X-Git-Tag: V_0_1_2_1~36
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=61811d33c5f860c0a145c63331f92448394107ed;p=helm.git

- de-ALB-ing
- added a debugging item for notation
---

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 0066d1c18..b9019a035 100644
--- 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> *)