From 649cc52200303abe4559d4c501c8aca06eed7591 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 12 Jun 2017 12:07:34 -0400
Subject: [travis overlay] Partially Revert 013c0232953f1f58

I've pushed commits which add `-bypass-API` to bedrock in the proper way, so these overlays are no longer needed---
 dev/ci/ci-basic-overlay.sh | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'dev/ci/ci-basic-overlay.sh')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 7a9df93c45..03cf0a9d14 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -97,14 +97,14 @@
 ########################################################################
 # bedrock_src
 ########################################################################
-: ${bedrock_src_CI_BRANCH:=trunk__API}
-: ${bedrock_src_CI_GITURL:=https://github.com/matejkosik/bedrock.git}
+: ${bedrock_src_CI_BRANCH:=master}
+: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
 
 ########################################################################
 # bedrock_facade
 ########################################################################
-: ${bedrock_facade_CI_BRANCH:=trunk__API}
-: ${bedrock_facade_CI_GITURL:=https://github.com/matejkosik/bedrock.git}
+: ${bedrock_facade_CI_BRANCH:=master}
+: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
 
 ########################################################################
 # formal-topology
-- 
cgit v1.2.3


From e36d139f6cb73d1e5021a77d38925b2879efda62 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 13 Jun 2017 17:24:43 +0200
Subject: Revert "[travis] temporary UniMath overlay"

This reverts commit 7ca4e36af8a12236a618bd3a8d045439df40dd43.

Not necessary anymore since UniMath/UniMath#715 has been merged.
---
 dev/ci/ci-basic-overlay.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev/ci/ci-basic-overlay.sh')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 3adc319355..d7714274e7 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -13,8 +13,8 @@
 ########################################################################
 # UniMath
 ########################################################################
-: ${UniMath_CI_BRANCH:=coq_makefile2-fix}
-: ${UniMath_CI_GITURL:=https://github.com/maximedenes/UniMath.git}
+: ${UniMath_CI_BRANCH:=master}
+: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}
 
 ########################################################################
 # Unicoq + Metacoq
-- 
cgit v1.2.3


From f4cec75fe74ff3f66f401efab357cae79124d984 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 14 Jun 2017 10:32:17 +0200
Subject: Temporary overlays because fewer plugins are loaded at startup.

---
 dev/ci/ci-basic-overlay.sh | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'dev/ci/ci-basic-overlay.sh')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 54db58c01f..b582921ecb 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -73,14 +73,14 @@
 ########################################################################
 # CompCert
 ########################################################################
-: ${CompCert_CI_BRANCH:=master}
-: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
+: ${CompCert_CI_BRANCH:=less_init_plugins}
+: ${CompCert_CI_GITURL:=https://github.com/letouzey/CompCert.git}
 
 ########################################################################
 # VST
 ########################################################################
-: ${VST_CI_BRANCH:=master}
-: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}
+: ${VST_CI_BRANCH:=less_init_plugins}
+: ${VST_CI_GITURL:=https://github.com/letouzey/VST.git}
 
 ########################################################################
 # fiat_parsers
@@ -91,8 +91,8 @@
 ########################################################################
 # fiat_crypto
 ########################################################################
-: ${fiat_crypto_CI_BRANCH:=master}
-: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}
+: ${fiat_crypto_CI_BRANCH:=less_init_plugins}
+: ${fiat_crypto_CI_GITURL:=https://github.com/letouzey/fiat-crypto.git}
 
 ########################################################################
 # bedrock_src
-- 
cgit v1.2.3


From c5dabed1c1f33005fe942882ea0fcf008d52784a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Jun 2017 11:45:45 +0200
Subject: Remove bedrock from test suite.

Bedrock relies on the 8.4 compat flag that we are removing, and we heard
from MIT that they did not plan to port bedrock to more recent versions
of Coq.
---
 dev/ci/ci-basic-overlay.sh | 12 ------------
 1 file changed, 12 deletions(-)

(limited to 'dev/ci/ci-basic-overlay.sh')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 7f66dfb3b0..0099e815f4 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -94,18 +94,6 @@
 : ${fiat_crypto_CI_BRANCH:=less_init_plugins}
 : ${fiat_crypto_CI_GITURL:=https://github.com/letouzey/fiat-crypto.git}
 
-########################################################################
-# bedrock_src
-########################################################################
-: ${bedrock_src_CI_BRANCH:=master}
-: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
-
-########################################################################
-# bedrock_facade
-########################################################################
-: ${bedrock_facade_CI_BRANCH:=master}
-: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
-
 ########################################################################
 # formal-topology
 ########################################################################
-- 
cgit v1.2.3