Nothing important

diff --git a/helm/EXPORT/export_Rocq_HIGMAN/Makefile b/helm/EXPORT/export_Rocq_HIGMAN/Makefile
index 0aaabeeec06ce4c3f08bf0d9f47b75d832f57fe3..f5161ba4ec093ec29ecd4880066b97a148817729 100644 (file)
--- a/helm/EXPORT/export_Rocq_HIGMAN/Makefile
+++ b/helm/EXPORT/export_Rocq_HIGMAN/Makefile
@@ -2,7 +2,7 @@ all: objects theories
 
 objects:
        coqc -R HIGMAN Rocq.HIGMAN HIGMAN/*.v
-       echo "Load Verbose prova_Rocq_HIGMAN." | ~/V7/bin/coqtop.byte -R HIGMAN Rocq.HIGMAN
+       echo "Load Verbose prova_Rocq_HIGMAN." | coqtop.byte -R HIGMAN Rocq.HIGMAN
 
 theories:
        ./exporttheories.sh

diff --git a/helm/EXPORT/export_Utrecht_Ramsey/Makefile b/helm/EXPORT/export_Utrecht_Ramsey/Makefile
index 2015d1755a57868c7ccf76818839bd660dac73a1..576b198db3be68ebfe91e7db0c8e1220f56622a8 100644 (file)
--- a/helm/EXPORT/export_Utrecht_Ramsey/Makefile
+++ b/helm/EXPORT/export_Utrecht_Ramsey/Makefile
@@ -2,7 +2,7 @@ all: objects theories
 
 objects:
        coqc -R Ramsey Utrecht.Ramsey Ramsey/*.v
-       echo "Load Verbose prova_Utrecht_Ramsey." | ~/V7/bin/coqtop.byte -R Ramsey Utrecht.Ramsey
+       echo "Load Verbose prova_Utrecht_Ramsey." | coqtop.byte -R Ramsey Utrecht.Ramsey
 
 theories:
        ./exporttheories.sh

diff --git a/helm/EXPORT/exportcoq/Makefile b/helm/EXPORT/exportcoq/Makefile
index 79c7463a046086eb5209a051ea5a58d61b2eeda7..5026ec526f835352a9053fa27bd82cb8a7d61f32 100644 (file)
--- a/helm/EXPORT/exportcoq/Makefile
+++ b/helm/EXPORT/exportcoq/Makefile
@@ -1,7 +1,7 @@
 all: objects theories
 
 objects:
-       echo "Load Verbose provacoq." | ~/V7/bin/coqtop.byte
+       echo "Load Verbose provacoq." | coqtop.byte
 
 theories:
        ./exporttheories.sh

diff --git a/helm/EXPORT/exportcoq/export_contrib_theory.sh b/helm/EXPORT/exportcoq/export_contrib_theory.sh
index 6ebb2ad281e00e3b7e648b97e116c8c04945e81a..afc191889666d6e2b5cb1124eb6d737720eb4adc 100755 (executable)
--- a/helm/EXPORT/exportcoq/export_contrib_theory.sh
+++ b/helm/EXPORT/exportcoq/export_contrib_theory.sh
@@ -2,7 +2,7 @@
 
 echo "Exporting theory $1";
 
-for i in ~/V7/contrib/$1/*.v
+for i in ../V7/contrib/$1/*.v
  do
   basename=$(basename $i | sed s/\\.v//)
   cat $i | ../mktheory.pl "Coq/$1/$basename" 0 > \

diff --git a/helm/EXPORT/exportcoq/export_theory_theory.sh b/helm/EXPORT/exportcoq/export_theory_theory.sh
index d2e5442bded8d68facaff15a3d96cbec6197c2bd..1a23583eb450eb9736cc2f846306e1153f1e8185 100755 (executable)
--- a/helm/EXPORT/exportcoq/export_theory_theory.sh
+++ b/helm/EXPORT/exportcoq/export_theory_theory.sh
@@ -2,7 +2,7 @@
 
 echo "Exporting theory $1";
 
-for i in ~/V7/theories/$1/*.v
+for i in ../V7/theories/$1/*.v
  do
   basename=$(basename $i | sed s/\\.v//)
   cat $i | ../mktheory.pl "Coq/$1/$basename" 0 > \

diff --git a/helm/EXPORT/exportprove/Makefile b/helm/EXPORT/exportprove/Makefile
index 28bb13d8a48a393d2b29f7552b4546dd5dee0565..4bd3a33e438dc78efe5a8802c47575f8c823b803 100644 (file)
--- a/helm/EXPORT/exportprove/Makefile
+++ b/helm/EXPORT/exportprove/Makefile
@@ -1,11 +1,11 @@
 all: objects theories
 
 objects:
-       coqc -R prove prove prove/*.v
-       echo "Load Verbose provaStruct." | ~/V7/bin/coqtop.byte -R prove prove
-       echo "Load Verbose provaFeIota." | ~/V7/bin/coqtop.byte -R prove prove
-       echo "Load Verbose provaCofix." | ~/V7/bin/coqtop.byte -R prove prove
-       echo "Load Verbose prova." | ~/V7/bin/coqtop.byte -R prove prove
+       coqc -R prove Bologna.prove prove/*.v
+       echo "Load Verbose provaStruct." | coqtop.byte -R prove Bologna.prove
+       echo "Load Verbose provaFeIota." | coqtop.byte -R prove Bologna.prove
+       echo "Load Verbose provaCofix." | coqtop.byte -R prove Bologna.prove
+       echo "Load Verbose prova." | coqtop.byte -R prove Bologna.prove
 
 theories:
        ./exporttheories.sh

diff --git a/helm/EXPORT/exportprove/exporttheories.sh b/helm/EXPORT/exportprove/exporttheories.sh
index f7993fe62bd484d039cc61cadeee10d86464f8a3..0b609bf56d32628f1b7ff54566e9082ce94b211b 100755 (executable)
--- a/helm/EXPORT/exportprove/exporttheories.sh
+++ b/helm/EXPORT/exportprove/exporttheories.sh
@@ -6,5 +6,5 @@ for i in prove/*.v
  do
   basename=$(basename $i | sed s/\\.v//)
   cat $i | ../mktheory.pl "prove/$basename" > \
-   examples/prove/$1/$basename.theory.xml
+   examples/Bologna/prove/$1/$basename.theory.xml
  done