From c70a21a1c522639138dbcfac53fb2ed96d731d98 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 12:05:04 +0200
Subject: [travis] fix CoLoR by inserting some Require Import FunInd

---
 dev/ci/ci-color.sh | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'dev')

diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 57f569858b..a0a4e0749d 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -18,4 +18,18 @@ sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${C
 sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v
 sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v
 
+# Adapt to PR #220 (FunInd not loaded in Prelude anymore)
+sed -i -e "15i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/basis/ordered_set.v
+sed -i -e "8i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/equational_extension.v
+sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/more_list_extention.v
+sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/ring_extention.v
+sed -i -e "27i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/dickson.v
+sed -i -e "26i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_permut.v
+sed -i -e "23i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_set.v
+sed -i -e "25i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_sort.v
+sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/more_list.v
+sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUtil.v
+sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v
+sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v
+
 ( cd ${Color_CI_DIR} && make -j ${NJOBS} )
-- 
cgit v1.2.3


From bba2186f781695db9d0987758119fde061499fbc Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 12:44:01 +0200
Subject: [travis] fix Software Foundation (one added Require Extraction)

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

(limited to 'dev')

diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 7d23ccad97..23ef41d2dd 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -7,6 +7,8 @@ source ${ci_dir}/ci-common.sh
 wget ${sf_CI_TARURL}
 tar xvfz sf.tgz
 
+sed -i.bak '15i From Coq Require Extraction.' sf/Extraction.v
+
 ( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} )
 
 
-- 
cgit v1.2.3


From 2470182ac4bded5c433c8f6bc77eb7b96576dc8d Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 14:48:22 +0200
Subject: [travis] overlays for CompCert and VST (an extra Require Export
 FunInd)

---
 dev/ci/ci-user-overlay.sh | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'dev')

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 200d431bcb..62c245b4fe 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -47,3 +47,10 @@ if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums"
     Corn_CI_BRANCH=external-bignums
     Corn_CI_GITURL=https://github.com/letouzey/corn.git
 fi
+
+if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins" ]; then
+    CompCert_CI_BRANCH=less_init_plugins
+    CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git
+    VST_CI_BRANCH=less_init_plugins
+    VST_CI_GITURL=https://github.com/letouzey/VST.git
+fi
-- 
cgit v1.2.3


From bb6dbba6a76f83c7cbac7a1f8d6eaa14da2d3d40 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 15:47:56 +0200
Subject: [travis] overlay for fiat-crypto (a Require Import FunInd)

---
 dev/ci/ci-user-overlay.sh | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev')

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 62c245b4fe..2ecd40416f 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -53,4 +53,6 @@ if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins"
     CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git
     VST_CI_BRANCH=less_init_plugins
     VST_CI_GITURL=https://github.com/letouzey/VST.git
+    fiat_crypto_CI_BRANCH=less_init_plugins
+    fiat_crypto_CI_GITURL=https://github.com/letouzey/fiat-crypto.git
 fi
-- 
cgit v1.2.3