Case c1 t1 vs c2 t2 where c1 and c2 are not splitted and t1 and t2

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

diff --git a/helm/EXPORT/export_Rocq_HIGMAN/Makefile b/helm/EXPORT/export_Rocq_HIGMAN/Makefile
index 0aaabeeec06ce4c3f08bf0d9f47b75d832f57fe3..f5161ba4ec093ec29ecd4880066b97a148817729 100644 (file)
--- 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