From 40e7943e21872051f6a88cba2a1e9faa6492b6a3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 20 Dec 2000 15:15:07 +0000 Subject: [PATCH] Nothing important --- helm/EXPORT/export_Rocq_HIGMAN/Makefile | 2 +- helm/EXPORT/export_Utrecht_Ramsey/Makefile | 2 +- helm/EXPORT/exportcoq/Makefile | 2 +- helm/EXPORT/exportcoq/export_contrib_theory.sh | 2 +- helm/EXPORT/exportcoq/export_theory_theory.sh | 2 +- helm/EXPORT/exportprove/Makefile | 10 +++++----- helm/EXPORT/exportprove/exporttheories.sh | 2 +- 7 files changed, 11 insertions(+), 11 deletions(-) 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 diff --git a/helm/EXPORT/export_Utrecht_Ramsey/Makefile b/helm/EXPORT/export_Utrecht_Ramsey/Makefile index 2015d1755..576b198db 100644 --- a/helm/EXPORT/export_Utrecht_Ramsey/Makefile +++ b/helm/EXPORT/export_Utrecht_Ramsey/Makefile @@ -2,7 +2,7 @@ all: objects theories objects: coqc -R Ramsey Utrecht.Ramsey Ramsey/*.v - echo "Load Verbose prova_Utrecht_Ramsey." | ~/V7/bin/coqtop.byte -R Ramsey Utrecht.Ramsey + echo "Load Verbose prova_Utrecht_Ramsey." | coqtop.byte -R Ramsey Utrecht.Ramsey theories: ./exporttheories.sh diff --git a/helm/EXPORT/exportcoq/Makefile b/helm/EXPORT/exportcoq/Makefile index 79c7463a0..5026ec526 100644 --- a/helm/EXPORT/exportcoq/Makefile +++ b/helm/EXPORT/exportcoq/Makefile @@ -1,7 +1,7 @@ all: objects theories objects: - echo "Load Verbose provacoq." | ~/V7/bin/coqtop.byte + echo "Load Verbose provacoq." | coqtop.byte theories: ./exporttheories.sh diff --git a/helm/EXPORT/exportcoq/export_contrib_theory.sh b/helm/EXPORT/exportcoq/export_contrib_theory.sh index 6ebb2ad28..afc191889 100755 --- a/helm/EXPORT/exportcoq/export_contrib_theory.sh +++ b/helm/EXPORT/exportcoq/export_contrib_theory.sh @@ -2,7 +2,7 @@ echo "Exporting theory $1"; -for i in ~/V7/contrib/$1/*.v +for i in ../V7/contrib/$1/*.v do basename=$(basename $i | sed s/\\.v//) cat $i | ../mktheory.pl "Coq/$1/$basename" 0 > \ diff --git a/helm/EXPORT/exportcoq/export_theory_theory.sh b/helm/EXPORT/exportcoq/export_theory_theory.sh index d2e5442bd..1a23583eb 100755 --- a/helm/EXPORT/exportcoq/export_theory_theory.sh +++ b/helm/EXPORT/exportcoq/export_theory_theory.sh @@ -2,7 +2,7 @@ echo "Exporting theory $1"; -for i in ~/V7/theories/$1/*.v +for i in ../V7/theories/$1/*.v do basename=$(basename $i | sed s/\\.v//) cat $i | ../mktheory.pl "Coq/$1/$basename" 0 > \ 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 diff --git a/helm/EXPORT/exportprove/exporttheories.sh b/helm/EXPORT/exportprove/exporttheories.sh index f7993fe62..0b609bf56 100755 --- a/helm/EXPORT/exportprove/exporttheories.sh +++ b/helm/EXPORT/exportprove/exporttheories.sh @@ -6,5 +6,5 @@ for i in prove/*.v do basename=$(basename $i | sed s/\\.v//) cat $i | ../mktheory.pl "prove/$basename" > \ - examples/prove/$1/$basename.theory.xml + examples/Bologna/prove/$1/$basename.theory.xml done -- 2.39.2