From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 20 Dec 2000 15:15:07 +0000 (+0000)
Subject: Nothing important
X-Git-Tag: nogzip~82
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=40e7943e21872051f6a88cba2a1e9faa6492b6a3;p=helm.git

Nothing important
---

diff --git a/helm/EXPORT/export_Rocq_HIGMAN/Makefile b/helm/EXPORT/export_Rocq_HIGMAN/Makefile
index 0aaabeeec..f5161ba4e 100644
--- 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 2015d1755..576b198db 100644
--- 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 79c7463a0..5026ec526 100644
--- 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 6ebb2ad28..afc191889 100755
--- 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 d2e5442bd..1a23583eb 100755
--- 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 28bb13d8a..4bd3a33e4 100644
--- 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 f7993fe62..0b609bf56 100755
--- 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