X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftptp_grafite%2Ftptp2grafite.ml;h=a7f3a85238fcf527172074b8266caf6396e1291b;hb=ce5018fb3004d79fd16301dfc0fd9370d59ba4fc;hp=3ed457d958dd64d25ee7d29ab111ad53574563c2;hpb=cd91767a396b7bbc72e6e3ee90a3b758421f935d;p=helm.git

diff --git a/components/tptp_grafite/tptp2grafite.ml b/components/tptp_grafite/tptp2grafite.ml
index 3ed457d95..a7f3a8523 100644
--- a/components/tptp_grafite/tptp2grafite.ml
+++ b/components/tptp_grafite/tptp2grafite.ml
@@ -247,7 +247,7 @@ let convert_ast statements context = function
           statements @ [
             GA.Executable(floc,GA.Command(floc,GA.Obj(floc,o)));
             GA.Executable(floc,GA.Tactic(floc, Some
-             (GA.Intros (floc,None,[])),GA.Dot(floc)))] @
+             (GA.Intros (floc,(None,[]))),GA.Dot(floc)))] @
           (if fv <> [] then     
             (List.flatten
               (List.map 
@@ -260,10 +260,10 @@ let convert_ast statements context = function
            else [])@
             [GA.Executable(floc,GA.Tactic(floc, Some (
               if ueq_case then
-                GA.Auto (floc,["paramodulation","";
+                GA.AutoBatch (floc,["paramodulation","";
                   "timeout",string_of_int !paramod_timeout])
               else
-                GA.Auto (floc,["depth",string_of_int !depth])
+                GA.AutoBatch (floc,["depth",string_of_int !depth])
             ),
               GA.Dot(floc)));
             GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,