From 61caf50dcc5e8da40952178ddea0b94cd70e334a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 14 May 2006 13:01:17 +0000
Subject: [PATCH] generation of more than one theorem per file fixed

---
 components/binaries/tptp2grafite/main.ml | 24 ++++++++----------------
 1 file changed, 8 insertions(+), 16 deletions(-)

diff --git a/components/binaries/tptp2grafite/main.ml b/components/binaries/tptp2grafite/main.ml
index 4ae496b1d..8df37fe00 100644
--- a/components/binaries/tptp2grafite/main.ml
+++ b/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
-- 
2.39.2