16 files changed, 23 insertions, 10 deletions
diff --git a/.travis.yml b/.travis.yml
index 196f4b22ad..8d70e346ad 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -39,6 +39,7 @@ env:
   - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
   - TEST_TARGET="validate"                           TW="travis_wait"
   - TEST_TARGET="validate"   COMPILER="4.02.3+32bit" TW="travis_wait"
+  - TEST_TARGET="validate"   COMPILER="4.05.0+flambda" CAMLP5_VER="7.01" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" NATIVE_COMP="no"
   - TEST_TARGET="ci-bignums TIMED=1"
   - TEST_TARGET="ci-color TIMED=1"
   - TEST_TARGET="ci-compcert TIMED=1"
@@ -103,6 +104,21 @@ matrix:
           - avsm
           packages: *extra-packages
 
+    # Full test-suite with flambda
+    - env:
+      - TEST_TARGET="test-suite"
+      - COMPILER="4.05.0+flambda"
+      - FINDLIB_VER="1.7.3"
+      - CAMLP5_VER="7.01"
+      - NATIVE_COMP="no"
+      - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3"
+      - EXTRA_OPAM="lablgtk-extras hevea"
+      addons:
+        apt:
+          sources:
+          - avsm
+          packages: *extra-packages
+
     # Ocaml warnings with two compilers
     - env:
       - TEST_TARGET="coqocaml"
@@ -143,7 +159,7 @@ matrix:
       - NATIVE_COMP="no"
       - COQ_DEST="-local"
       before_install:
-      - brew update --debug --verbose
+      - brew update
       - brew install opam gnu-time
 
     - if: NOT (type = pull_request)
@@ -157,7 +173,7 @@ matrix:
       - EXTRA_CONF="-coqide opt -warn-error"
       - EXTRA_OPAM="lablgtk-extras"
       before_install:
-      - brew update --debug --verbose
+      - brew update
       - brew install opam gnu-time gtk+ expat gtksourceview libxml2 gdk-pixbuf python3
       - pip3 install macpack
       before_deploy:
diff --git a/README.md b/README.md
index 03f24071b8..2ad5122156 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 # Coq
 
-[![Travis](https://travis-ci.org/coq/coq.svg?branch=master)](https://travis-ci.org/coq/coq/builds) [![Gitter](https://badges.gitter.im/coq/coq.svg)](https://gitter.im/coq/coq)
+[![Travis](https://travis-ci.org/coq/coq.svg?branch=master)](https://travis-ci.org/coq/coq/builds) [![Build status](https://ci.appveyor.com/api/projects/status/eln43k05pa2vm908/branch/master?svg=true)](https://ci.appveyor.com/project/coq/coq/branch/master) [![Gitter](https://badges.gitter.im/coq/coq.svg)](https://gitter.im/coq/coq)
 
 Coq is a formal proof management system. It provides a formal language to write
 mathematical definitions, executable algorithms and theorems together with an
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 545846da58..9be882bb3c 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -49,11 +49,8 @@
 ########################################################################
 # HoTT
 ########################################################################
-# Temporary overlay
-: ${HoTT_CI_BRANCH:=ocaml.4.02.3}
-: ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git}
-# : ${HoTT_CI_BRANCH:=master}
-# : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}
+: ${HoTT_CI_BRANCH:=master}
+: ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}
 
 ########################################################################
 # GeoCoq
@@ -76,8 +73,8 @@
 ########################################################################
 # CompCert
 ########################################################################
-: ${CompCert_CI_BRANCH:=less_init_plugins}
-: ${CompCert_CI_GITURL:=https://github.com/letouzey/CompCert.git}
+: ${CompCert_CI_BRANCH:=master}
+: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
 
 ########################################################################
 # VST
diff --git a/test-suite/bugs/closed/38.v b/test-suite/bugs/closed/1238.v
index 6b6e83779f..6b6e83779f 100644
--- a/test-suite/bugs/closed/38.v
+++ b/test-suite/bugs/closed/1238.v
diff --git a/test-suite/bugs/closed/121.v b/test-suite/bugs/closed/1341.v
index 8c5a38859f..8c5a38859f 100644
--- a/test-suite/bugs/closed/121.v
+++ b/test-suite/bugs/closed/1341.v
diff --git a/test-suite/bugs/closed/148.v b/test-suite/bugs/closed/1362.v
index 6cafb9f0cd..6cafb9f0cd 100644
--- a/test-suite/bugs/closed/148.v
+++ b/test-suite/bugs/closed/1362.v
diff --git a/test-suite/bugs/closed/328.v b/test-suite/bugs/closed/1542.v
index 52cfbbc496..52cfbbc496 100644
--- a/test-suite/bugs/closed/328.v
+++ b/test-suite/bugs/closed/1542.v
diff --git a/test-suite/bugs/closed/329.v b/test-suite/bugs/closed/1543.v
index def6ed98dd..def6ed98dd 100644
--- a/test-suite/bugs/closed/329.v
+++ b/test-suite/bugs/closed/1543.v
diff --git a/test-suite/bugs/closed/331.v b/test-suite/bugs/closed/1545.v
index 9ef796faf7..9ef796faf7 100644
--- a/test-suite/bugs/closed/331.v
+++ b/test-suite/bugs/closed/1545.v
diff --git a/test-suite/bugs/closed/335.v b/test-suite/bugs/closed/1547.v
index 166fa7a9f2..166fa7a9f2 100644
--- a/test-suite/bugs/closed/335.v
+++ b/test-suite/bugs/closed/1547.v
diff --git a/test-suite/bugs/closed/348.v b/test-suite/bugs/closed/1551.v
index 48f0b55129..48f0b55129 100644
--- a/test-suite/bugs/closed/348.v
+++ b/test-suite/bugs/closed/1551.v
diff --git a/test-suite/bugs/closed/545.v b/test-suite/bugs/closed/1584.v
index 926af7dd1c..926af7dd1c 100644
--- a/test-suite/bugs/closed/545.v
+++ b/test-suite/bugs/closed/1584.v
diff --git a/test-suite/bugs/closed/846.v b/test-suite/bugs/closed/5797.v
index ee5ec1fa6a..ee5ec1fa6a 100644
--- a/test-suite/bugs/closed/846.v
+++ b/test-suite/bugs/closed/5797.v
diff --git a/test-suite/bugs/closed/931.v b/test-suite/bugs/closed/5845.v
index ea3347a851..ea3347a851 100644
--- a/test-suite/bugs/closed/931.v
+++ b/test-suite/bugs/closed/5845.v
diff --git a/test-suite/bugs/closed/1100.v b/test-suite/bugs/closed/5940.v
index 32c78b4b9e..32c78b4b9e 100644
--- a/test-suite/bugs/closed/1100.v
+++ b/test-suite/bugs/closed/5940.v
diff --git a/test-suite/bugs/opened/743.v b/test-suite/bugs/opened/1615.v
index 2825701410..2825701410 100644
--- a/test-suite/bugs/opened/743.v
+++ b/test-suite/bugs/opened/1615.v