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 d79c2661dbcdea785e51ae4af7f599e5a8cb090e..071bf8ddb8874215000070cfbe2a4fc28942dd5d 100644 (file)
--- 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 b7efd6820bcf464d8a0fa88750b6621336ec7ecd..51c7bbe482c2b0b2b4d4eac0db8769d89251365a 100644 (file)
--- 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