X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FEXPORT%2Fexport_Rocq_HIGMAN%2FMakefile;h=f5161ba4ec093ec29ecd4880066b97a148817729;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=0aaabeeec06ce4c3f08bf0d9f47b75d832f57fe3;hpb=b553fcede2e5173922ebb86abf1661422ac567d5;p=helm.git

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