X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FEXPORT%2Fexportprove%2FMakefile;h=4bd3a33e438dc78efe5a8802c47575f8c823b803;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=28bb13d8a48a393d2b29f7552b4546dd5dee0565;hpb=5cc1f56f25e23f8132b578f9ad46ac9e27979cb4;p=helm.git

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