From 61811d33c5f860c0a145c63331f92448394107ed Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 12 Sep 2005 16:36:27 +0000 Subject: [PATCH] - de-ALB-ing - added a debugging item for notation --- helm/matita/matita.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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 (** *) -- 2.39.2