diff options
| author |  Jasper Hugunin <jasperh@cs.washington.edu> | 2018-03-29 13:56:37 -0700 |
|---|---|---|
| committer | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-03-29 13:56:37 -0700 |
| commit | b125a5f28b41c5a8f9fb3d5944f7b9a1bad0ba24 (patch) | |
| tree | 3038dfe4461fb429b6bc867b067eb03d565cd034 | |
| parent | c0eedb5bdcb815132f404e19d6bf59730ae6e2df (diff) | |
Remove outdated patch from ci-sf
| -rwxr-xr-x | dev/ci/ci-sf.sh | 19 |
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 ) |