X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.ml;h=dd8d6d83dad6a115d6e13540a44fc128ca8c0cb7;hb=6fa89cef6aa8fc1774db065a9fcfc47867579054;hp=b9e09f24d8dbc88bcbbaa4ca05c4ca30dc71e4c7;hpb=9e8c5d2163e701413517153f00a52dac1cd31ecd;p=helm.git

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index b9e09f24d..dd8d6d83d 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -30,7 +30,8 @@ open MatitaTypes
 
 (** {2 Initialization} *)
 
-let _ = MatitaInit.initialize_all () 
+let _ = MatitaInit.initialize_all ()
+let _ = Paramodulation.Saturation.init () (* ALB to link paramodulation *)
 
 (** {2 GUI callbacks} *)
 
@@ -153,7 +154,16 @@ let _ =
           (List.map (fun (g, _, _) -> string_of_int g)
             (MatitaScript.current ())#proofMetasenv));
         prerr_endline ("stack: " ^ Continuationals.Stack.pp
-          (MatitaMisc.get_stack (MatitaScript.current ())#status)));
+          (MatitaTypes.get_stack (MatitaScript.current ())#status)));
+(*     addDebugItem "ask record choice"
+      (fun _ ->
+        MatitaLog.debug (string_of_int
+          (MatitaGtkMisc.ask_record_choice ~gui ~title:"title" ~message:"msg"
+          ~fields:["a"; "b"; "c"]
+          ~records:[
+            ["0"; "0"; "0"]; ["0"; "0"; "1"]; ["0"; "1"; "0"]; ["0"; "1"; "1"];
+            ["1"; "0"; "0"]; ["1"; "0"; "1"]; ["1"; "1"; "0"]; ["1"; "1"; "1"]]
+          ()))); *)
     addDebugItem "rotate light bulbs"
       (fun _ ->
          let nb = gui#main#hintNotebook in