From a8700ca77511655526bd40e46b76128853ce6b0c Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 15 Jun 2006 09:22:29 +0000
Subject: [PATCH] default constants are now the matita standard library ones
 and not the one from Coq. the makefile should work on every checkout, since
 the path for the TPTP stuff is not hardcoded, but ppoint to the TPTP-VERSION/
 directory in the user's home.

---
 helm/software/components/binaries/tptp2grafite/Makefile | 6 +++---
 helm/software/components/binaries/tptp2grafite/main.ml  | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/helm/software/components/binaries/tptp2grafite/Makefile b/helm/software/components/binaries/tptp2grafite/Makefile
index d79c2661d..071bf8ddb 100644
--- a/helm/software/components/binaries/tptp2grafite/Makefile
+++ b/helm/software/components/binaries/tptp2grafite/Makefile
@@ -1,5 +1,5 @@
 OCAMLC = OCAMLPATH=../../METAS ocamlfind ocamlc -package helm-grafite_parser
-TPTPDIR=/home/tassi/helm/trunk/TPTP-v3.1.1/
+TPTPDIR=/home/$(USER)/TPTP-v3.1.1/
 
 opt all: tptp2grafite
 	echo -n
@@ -27,13 +27,13 @@ testall: tptp2grafite
 
 generate:
 	for X in `cat unit_equality_problems`; do\
-		./tptp2grafite -tptppath /home/tassi/TPTP-v3.1.1/ $$X \
+		./tptp2grafite -tptppath $(TPTPDIR) $$X \
 		> ../../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
 	done
 
 parse:
 	for X in `cat unit_equality_problems`; do\
 	  echo "Parsing $$X"; \
-		./tptp2grafite -tptppath /home/tassi/TPTP-v3.1.1/ $$X \
+		./tptp2grafite -tptppath $(TPTPDIR) $$X \
 		> /dev/null || echo Failed: $$X; \
 	done
diff --git a/helm/software/components/binaries/tptp2grafite/main.ml b/helm/software/components/binaries/tptp2grafite/main.ml
index b7efd6820..51c7bbe48 100644
--- a/helm/software/components/binaries/tptp2grafite/main.ml
+++ b/helm/software/components/binaries/tptp2grafite/main.ml
@@ -305,7 +305,7 @@ let _ =
   let extra_statements_start = [
     GA.Executable(floc,GA.Command(floc,
       GA.Set(floc,"baseuri","cic:/matita/TPTP/" ^ !inputfile)));
-    GA.Executable(floc,GA.Command(floc, GA.Include(floc,"legacy/coq.ma")))]
+    GA.Executable(floc,GA.Command(floc, GA.Include(floc,"library_notation.ma")))]
   in
   List.iter pp extra_statements_start;
   List.iter 
@@ -314,11 +314,11 @@ let _ =
     (LexiconAstPp.pp_command 
       (LA.Alias(floc,
         LA.Ident_alias(n,s))) ^ "."))
-   [("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)");
+   [(*("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)");
    ("trans_eq","cic:/Coq/Init/Logic/trans_eq.con");
    ("eq_ind_r","cic:/Coq/Init/Logic/eq_ind_r.con");
    ("eq_ind","cic:/Coq/Init/Logic/eq_ind.con");
    ("sym_eq","cic:/Coq/Init/Logic/sym_eq.con");
-   ("refl_equal","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)")];
+   ("refl_equal","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)") *)];
   List.iter pp grafite_ast_statements;
   exit 0
-- 
2.39.2