X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftptp2grafite%2Fmain.ml;fp=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftptp2grafite%2Fmain.ml;h=8df37fe00e3154f6fd58625bbc24a81ebdb082e8;hb=9b8ad1220893070c9a98500f99355bba7775743d;hp=4ae496b1da3270ac7c8ff92330d8d586356094e5;hpb=7242219e9c4934ed347d23dc7a66fbb280a117e1;p=helm.git

diff --git a/helm/software/components/binaries/tptp2grafite/main.ml b/helm/software/components/binaries/tptp2grafite/main.ml
index 4ae496b1d..8df37fe00 100644
--- a/helm/software/components/binaries/tptp2grafite/main.ml
+++ b/helm/software/components/binaries/tptp2grafite/main.ml
@@ -152,9 +152,13 @@ let convert_ast statements context = function
           in
           let o = PT.Theorem (`Theorem,name,f,None) in
           statements @ [
-            GA.Executable(
-              floc,GA.Command(
-                floc,GA.Obj(floc,o)))],
+            GA.Executable(floc,GA.Command(floc,GA.Obj(floc,o)));
+            GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
+              GA.Intros (floc,None,[])),Some (GA.Dot(floc))));
+            GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
+              GA.Auto (floc,None,None,Some "paramodulation",None)),
+                Some (GA.Dot(floc))));
+            GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))],
           context
       | A.Definition 
       | A.Lemma 
@@ -225,10 +229,7 @@ let _ =
   in
   let pp t = 
     (* for a correct pp we should disambiguate the term... *)
-    let term_pp x = 
-      BoxPp.render_to_string 80 (CicNotationPres.render (Hashtbl.create 1)
-        (TermContentPres.pp_ast x))
-    in
+    let term_pp = CicNotationPp.pp_term in
     let lazy_term_pp = fun x -> assert false in
     let obj_pp = CicNotationPp.pp_obj in
     print_endline 
@@ -239,19 +240,10 @@ let _ =
       GA.Set(floc,"baseuri","cic:/matita/TPTP/" ^ !inputfile)));
     GA.Executable(floc,GA.Command(floc, GA.Include(floc,"legacy/coq.ma")))]
   in
-  let extra_statements_end = [
-    GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
-      GA.Intros (floc,None,[])),Some (GA.Dot(floc))));
-    GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
-      GA.Auto (floc,None,None,Some "paramodulation",None)),
-      Some (GA.Dot(floc))));
-    GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))]
-  in 
   List.iter pp extra_statements_start;
   print_endline
     (LexiconAstPp.pp_command 
       (LA.Alias(floc,
         LA.Ident_alias("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"))) ^ ".");
   List.iter pp grafite_ast_statements;
-  List.iter pp extra_statements_end;
   exit 0