X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2Ftptp2grafite.ml;h=a19fa67c20d3281967d8ec77a754f84ede510a51;hb=5d0d8107649b9264ebe7d8ff2c69bf777179b0d2;hp=7950ca15d4e25e329ef2f3f331c6b2b082b5a7c0;hpb=0639dda9142d1cf047b07e61fb557e8877aba4d8;p=helm.git

diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml
index 7950ca15d..a19fa67c2 100644
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -221,7 +221,8 @@ let ng_generate_tactics fv ueq_case context arities =
   (HExtlib.list_mapi
    (fun (name,_) _-> 
      GA.Executable(floc,GA.NTactic(floc, 
-      [GA.NIntro (floc,name);GA.NDot(floc)])))
+      [GA.NIntro (floc,(try List.assoc name kw with Not_found -> name));
+       GA.NDot(floc)])))
    arities)
   @
   (HExtlib.list_mapi
@@ -272,7 +273,9 @@ let ng_generate_tactics fv ueq_case context arities =
                GA.NSkip floc; GA.NMerge floc]))])
       fv)) 
  else [])@
-  [GA.Executable(floc,GA.Command(floc, GA.NQed(floc)))]
+    [GA.Executable(floc,GA.NTactic(floc,[GA.NTry(floc, GA.NAssumption(floc));
+					 GA.NSemicolon(floc)]))]@
+  [GA.Executable(floc,GA.NCommand(floc, GA.NQed(floc)))]
 ;;
 
 let generate_tactics fv ueq_case =
@@ -437,8 +440,9 @@ let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filenam
   let preamble = 
     match raw_preamble with
     | None -> 
-       pp (GA.Executable(floc,
-           GA.Command(floc,GA.Include(floc,true,"logic/equality.ma"))))
+      pp
+       (GA.Executable(floc,
+         GA.Command(floc,GA.Include(floc,true,`OldAndNew,"logic/equality.ma"))))
     | Some s -> s buri
   in
   let extra_statements_end = [] in