From c67a6aaf5f24719785eb170e1fdef97c180e927e 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.

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

diff --git a/components/binaries/tptp2grafite/Makefile b/components/binaries/tptp2grafite/Makefile
index d79c2661d..071bf8ddb 100644
--- a/components/binaries/tptp2grafite/Makefile
+++ b/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/components/binaries/tptp2grafite/main.ml b/components/binaries/tptp2grafite/main.ml
index b7efd6820..51c7bbe48 100644
--- a/components/binaries/tptp2grafite/main.ml
+++ b/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