From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 15 Jun 2006 09:22:29 +0000 (+0000)
Subject: default constants are now the matita standard library ones and not the one from Coq.
X-Git-Tag: make_still_working~7184
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a8700ca77511655526bd40e46b76128853ce6b0c;p=helm.git

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

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