summaryrefslogtreecommitdiff
path: root/dev/ci/ci-sf.sh
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci/ci-sf.sh')
-rwxr-xr-xdev/ci/ci-sf.sh9
1 files changed, 2 insertions, 7 deletions
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 58bbb722..60436e67 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -8,11 +8,6 @@ wget -qO- "${sf_lf_CI_TARURL}" | tar xvz
wget -qO- "${sf_plf_CI_TARURL}" | tar xvz
wget -qO- "${sf_vfa_CI_TARURL}" | tar xvz
-sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v
-sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v
-
-( cd lf && make clean && make )
-
-( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make )
-
+( cd lf && make clean && make )
+( cd plf && make clean && make )
( cd vfa && make clean && make )