X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2Ftptp2grafite.ml;h=c63fca74166bfc137203a91e4033d90040a6c4db;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=2e1bb9bce2d93cfbdb1e0f964e5dd3214bc87f2d;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml
index 2e1bb9bce..c63fca741 100644
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -246,14 +246,14 @@ let ng_generate_tactics fv ueq_case context arities =
  else [])@
   [GA.Executable(floc,GA.NTactic(floc, [
     if (*ueq_case*) true then
-        GA.NAuto (floc,(Some 
+        GA.NAuto (floc,(
           HExtlib.list_mapi 
             (fun _ i -> 
                mk_ident ("H" ^ string_of_int i)) 
             context    
                 ,[]))
     else
-        GA.NAuto (floc,(None,[
+        GA.NAuto (floc,([],[
                 "depth",string_of_int 5;
                 "width",string_of_int 5;
                 "size",string_of_int 20;
@@ -294,10 +294,10 @@ let generate_tactics fv ueq_case =
  else [])@
   [GA.Executable(floc,GA.Tactic(floc, Some (
     if true (*ueq_case*) then
-        GA.AutoBatch (floc,(None,["paramodulation","";
+        GA.AutoBatch (floc,([],["paramodulation","";
         "timeout",string_of_int !paramod_timeout]))
     else
-        GA.AutoBatch (floc,(None,[
+        GA.AutoBatch (floc,([],[
                 "depth",string_of_int 5;
                 "width",string_of_int 5;
                 "size",string_of_int 20;