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

diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml
index a19fa67c2..2e1bb9bce 100644
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -237,22 +237,23 @@ let ng_generate_tactics fv ueq_case context arities =
       (fun _ -> 
         [GA.Executable(floc,GA.NTactic(floc, 
           [GA.NApply (floc,
-            PT.Appl [mk_ident "ex_intro";PT.Implicit;PT.Implicit;
-              PT.Implicit;PT.Implicit]);GA.NBranch floc]));
+            PT.Appl
+             [mk_ident "ex_intro";PT.Implicit `JustOne;PT.Implicit `JustOne;
+              PT.Implicit `JustOne;PT.Implicit `JustOne]);GA.NBranch floc]));
          GA.Executable(floc,GA.NTactic(floc, 
           [GA.NPos (floc,[2])]))])
       fv)) 
  else [])@
   [GA.Executable(floc,GA.NTactic(floc, [
     if (*ueq_case*) true then
-        GA.NAuto (floc,(
+        GA.NAuto (floc,(Some 
           HExtlib.list_mapi 
             (fun _ i -> 
                mk_ident ("H" ^ string_of_int i)) 
             context    
                 ,[]))
     else
-        GA.NAuto (floc,([],[
+        GA.NAuto (floc,(None,[
                 "depth",string_of_int 5;
                 "width",string_of_int 5;
                 "size",string_of_int 20;
@@ -293,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,([],["paramodulation","";
+        GA.AutoBatch (floc,(None,["paramodulation","";
         "timeout",string_of_int !paramod_timeout]))
     else
-        GA.AutoBatch (floc,([],[
+        GA.AutoBatch (floc,(None,[
                 "depth",string_of_int 5;
                 "width",string_of_int 5;
                 "size",string_of_int 20;
@@ -353,7 +354,7 @@ let convert_ast ng statements context = function
                (mk_ident universe,Some (PT.Sort (`Type (CicUniv.fresh ())))), 
                convert_formula fv false context f)
           in
-          let o = PT.Theorem (`Theorem,name,f,None) in
+          let o = PT.Theorem (`Theorem,name,f,None,`Regular) in
           (statements @ 
           [ GA.Executable(floc,GA.Command(floc,
              (*if ng then GA.NObj (floc,o) else*) GA.Obj(floc,o))); ] @