From c5f9e3a03c1f089253622ec262adf931e6dc1ca2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Nov 2017 15:00:38 +0100
Subject: Adding ad hoc overlay for sf/vfa.

---
 dev/ci/ci-sf.sh | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'dev')

diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 272041205c..217540cc19 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -14,6 +14,25 @@ tar xvfz vfa.tgz
 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 )
-- 
cgit v1.2.3