ocaml 3.09 transition

[helm.git] / helm / EXPORT / exportprove / Makefile

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