7 files changed, 0 insertions, 46 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index d5351f573..1de9e7f7c 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -244,12 +244,6 @@ validate:32bit:
 ci-bignums:
   <<: *ci-template
 
-ci-bedrock-src:
-  <<: *ci-template
-
-ci-bedrock-facade:
-  <<: *ci-template
-
 ci-color:
   <<: *ci-template
   variables:
diff --git a/.travis.yml b/.travis.yml
index 01680583f..224dfe2f5 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -38,8 +38,6 @@ env:
   - TEST_TARGET="validate"                           TW="travis_wait"
   - TEST_TARGET="validate"   COMPILER="4.02.3+32bit" TW="travis_wait"
   - TEST_TARGET="ci-bignums"
-  - TEST_TARGET="ci-bedrock-src"
-  - TEST_TARGET="ci-bedrock-facade"
   - TEST_TARGET="ci-color"
   - TEST_TARGET="ci-compcert"
   - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
diff --git a/Makefile.ci b/Makefile.ci
index 2f7fcd48a..3be90c0a3 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -1,7 +1,5 @@
 CI_TARGETS=ci-all \
     ci-bignums \
-    ci-bedrock-facade \
-    ci-bedrock-src \
     ci-color \
     ci-compcert \
     ci-coq-dpdgraph \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 7f66dfb3b..0099e815f 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -95,18 +95,6 @@
 : ${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
 ########################################################################
 : ${formal_topology_CI_BRANCH:=ci}
diff --git a/dev/ci/ci-bedrock-facade.sh b/dev/ci/ci-bedrock-facade.sh
deleted file mode 100755
index 95cfa3073..000000000
--- a/dev/ci/ci-bedrock-facade.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
-
-bedrock_facade_CI_DIR=${CI_BUILD_DIR}/bedrock-facade
-
-git_checkout ${bedrock_facade_CI_BRANCH} ${bedrock_facade_CI_GITURL} ${bedrock_facade_CI_DIR}
-
-( cd ${bedrock_facade_CI_DIR} && make -j ${NJOBS} facade )
diff --git a/dev/ci/ci-bedrock-src.sh b/dev/ci/ci-bedrock-src.sh
deleted file mode 100755
index 532611d4b..000000000
--- a/dev/ci/ci-bedrock-src.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
-
-bedrock_src_CI_DIR=${CI_BUILD_DIR}/bedrock-src
-
-git_checkout ${bedrock_src_CI_BRANCH} ${bedrock_src_CI_GITURL} ${bedrock_src_CI_DIR}
-
-( cd ${bedrock_src_CI_DIR} && make -j ${NJOBS} src )
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 2ecd40416..b242ce3bd 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -33,10 +33,6 @@ fi
 echo "DEBUG: ci-user-overlay.sh 0"
 if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then
     echo "DEBUG: ci-user-overlay.sh 1"
-    bedrock_src_CI_BRANCH=trunk__API
-    bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git
-    bedrock_facade_CI_BRANCH=trunk__API
-    bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git
     fiat_parsers_CI_BRANCH=trunk__API
     fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git
 fi