]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/EXPORT/export_Rocq_HIGMAN/Makefile
ocaml 3.09 transition
[helm.git] / helm / EXPORT / export_Rocq_HIGMAN / Makefile
index 0aaabeeec06ce4c3f08bf0d9f47b75d832f57fe3..f5161ba4ec093ec29ecd4880066b97a148817729 100644 (file)
@@ -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