aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Jasper Hugunin <jasperh@cs.washington.edu>2018-03-29 13:56:37 -0700
committerGravatar Jasper Hugunin <jasperh@cs.washington.edu>2018-03-29 13:56:37 -0700
commitb125a5f28b41c5a8f9fb3d5944f7b9a1bad0ba24 (patch)
tree3038dfe4461fb429b6bc867b067eb03d565cd034 /dev
parentc0eedb5bdcb815132f404e19d6bf59730ae6e2df (diff)
Remove outdated patch from ci-sf
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/ci-sf.sh19
1 files changed, 0 insertions, 19 deletions
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 4e8c7e145..4f7e9517f 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -11,25 +11,6 @@ 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
-# Delete useless calls to try omega; unfold
-patch vfa/SearchTree.v <<EOF
-*** SearchTree.v.bak 2017-09-06 19:12:59.000000000 +0200
---- SearchTree.v 2017-11-21 16:34:41.000000000 +0100
-***************
-*** 674,683 ****
- forall i j : key, ~ (i > j) -> ~ (i < j) -> i=j.
- Proof.
- intros.
-- try omega. (* Oops! [omega] cannot solve this one.
-- The problem is that [i] and [j] have type [key] instead of type [nat].
-- The solution is easy enough: *)
-- unfold key in *.
- omega.
-
- (** So, if you get stuck on an [omega] that ought to work,
---- 674,679 ----
-EOF
-
( cd lf && make clean && make )
( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make )