Merge PR #7121: Remove outdated patch from ci-sf

1 files changed, 0 insertions, 19 deletions

diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 4e8c7e145e..4f7e9517f4 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 )