Enrico Tassi · Benjamin Barenblat · Benjamin Barenblat · Benjamin Barenblat · Benjamin Barenblat · Benjamin Barenblat
--- a/.bintray.json
+++ b/.bintray.json
+{
+    "package": {
+        "name": "coq",
+        "repo": "coq",
+        "subject": "coq"
+    },
+
+    "version": {
+        "name": "8.8.2"
+    },
+
+    "files":
+        [
+        {"includePattern": "_build/(.*\\.dmg)", "uploadPattern": "$1",
+         "matrixParams": {
+             "override": 1 }
+        }
+        ],
+    "publish": true
+}
--- a/.gitattributes
+++ b/.gitattributes
-.dir-locals.el export-ignore
-.gitattributes export-ignore
-.gitignore export-ignore
-.mailmap export-ignore
-TODO export-ignore
--- a/.github/ISSUE_TEMPLATE.md
+++ b/.github/ISSUE_TEMPLATE.md
+<!-- Thank you for your contribution.
+     Please complete the following information when reporting a bug. -->
+
+#### Version
+
+<!-- You can get this information by running `coqtop -v`. -->
+
+
+#### Operating system
+
+
+#### Description of the problem
+
+<!-- It is helpful to provide enough information so that we can reproduce the bug.
+     In particular, please include a code example which produces it.
+     If the example is small, you can include it here between ``` ```.
+     Otherwise, please provide a link to a repository, a gist (https://gist.github.com)
+     or drag-and-drop a `.zip` archive. -->
--- a/.github/PULL_REQUEST_TEMPLATE.md
+++ b/.github/PULL_REQUEST_TEMPLATE.md
+<!-- Thank you for your contribution.
+     Make sure you read the contributing guide and fill this template. -->
+
+
+<!-- Keep what applies -->
+**Kind:** documentation / bug fix / feature / performance / infrastructure.
+
+
+<!-- If this is a bug fix, make sure the bug was reported beforehand. -->
+Fixes / closes #????
+
+
+<!-- If this is a feature pull request / breaks compatibility: -->
+<!-- (Otherwise, remove these lines.) -->
+- [ ] Corresponding documentation was added / updated.
+- [ ] Entry added in CHANGES.
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
+image: "$IMAGE"
+
+stages:
+  - docker
+  - build
+  - test
+
+# some default values
+variables:
+  # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
+  # for reference]
+  CACHEKEY: "bionic_coq-v8.8-V2018-09-20"
+  IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
+  # By default, jobs run in the base switch; override to select another switch
+  OPAM_SWITCH: "base"
+  # Used to select special compiler switches such as flambda, 32bits, etc...
+  OPAM_VARIANT: ""
+
+docker-boot:
+  stage: docker
+  image: docker:stable
+  services:
+    - docker:dind
+  before_script: []
+  script:
+    - docker login -u gitlab-ci-token -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
+    - cd dev/ci/docker/bionic_coq/
+    - if docker pull "$IMAGE"; then echo "Image prebuilt!"; exit 0; fi
+    - docker build -t "$IMAGE" .
+    - docker push "$IMAGE"
+  except:
+    variables:
+      - $SKIP_DOCKER == "true"
+  tags:
+    - docker
+
+before_script:
+  - cat /proc/{cpu,mem}info || true
+  - ls -a # figure out if artifacts are around
+  - printenv | sort
+  - declare -A switch_table
+  - switch_table=( ["base"]="$COMPILER" ["edge"]="$COMPILER_EDGE" )
+  - opam switch -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT"
+  - eval $(opam config env)
+  - opam list
+  - opam config list
+
+after_script:
+  - echo "The build completed normally (not a runner failure)."
+
+################ GITLAB CACHING ######################
+# - use artifacts between jobs                       #
+######################################################
+
+# TODO figure out how to build doc for installed Coq
+.build-template: &build-template
+  stage: build
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - _install_ci
+      - config/Makefile
+      - test-suite/misc/universes/all_stdlib.v
+    expire_in: 1 week
+  script:
+    - set -e
+
+    - echo 'start:coq.config'
+    - ./configure -warn-error yes -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE"
+    - echo 'end:coq.config'
+
+    - echo 'start:coq.build'
+    - make -j "$NJOBS" byte
+    - make -j "$NJOBS"
+    - make test-suite/misc/universes/all_stdlib.v
+    - echo 'end:coq:build'
+
+    - echo 'start:coq.install'
+    - make install
+    - make install-byte
+    - cp bin/fake_ide _install_ci/bin/
+    - echo 'end:coq.install'
+
+    - set +e
+
+# every non build job must set dependencies otherwise all build
+# artifacts are used together and we may get some random Coq. To that
+# purpose, we add a spurious dependency `not-a-real-job` that must be
+# overridden otherwise the CI will fail.
+
+# set dependencies when using
+.test-suite-template: &test-suite-template
+  stage: test
+  dependencies:
+    - not-a-real-job
+  script:
+    - cd test-suite
+    - make clean
+    # careful with the ending /
+    - BIN=$(readlink -f ../_install_ci/bin)/
+    - LIB=$(readlink -f ../_install_ci/lib/coq)/
+    - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" all
+  artifacts:
+    name: "$CI_JOB_NAME.logs"
+    when: on_failure
+    paths:
+      - test-suite/logs
+
+# set dependencies when using
+.validate-template: &validate-template
+  stage: test
+  dependencies:
+    - not-a-real-job
+  script:
+    - cd _install_ci
+    - find lib/coq/ -name '*.vo' -print0 > vofiles
+    - for regexp in 's/.vo//' 's:lib/coq/plugins:Coq:' 's:lib/coq/theories:Coq:' 's:/:.:g'; do sed -z -i "$regexp" vofiles; done
+    - xargs -0 --arg-file=vofiles bin/coqchk -boot -silent -o -m -coqlib lib/coq/
+
+.ci-template: &ci-template
+  stage: test
+  script:
+    - set -e
+    - echo 'start:coq.test'
+    - make -f Makefile.ci -j "$NJOBS" ${TEST_TARGET}
+    - echo 'end:coq.test'
+    - set +e
+  dependencies:
+    - build:base
+  variables: &ci-template-vars
+    TEST_TARGET: "$CI_JOB_NAME"
+
+.ci-template-flambda: &ci-template-flambda
+  <<: *ci-template
+  dependencies:
+    - build:edge+flambda
+  variables:
+    <<: *ci-template-vars
+    OPAM_SWITCH: "edge"
+    OPAM_VARIANT: "+flambda"
+
+.windows-template: &windows-template
+  stage: test
+  artifacts:
+    name: "%CI_JOB_NAME%"
+    paths:
+      - artifacts
+    when: always
+    expire_in: 1 week
+  dependencies: []
+  tags:
+    - windows
+  before_script: []
+  script:
+    - call dev/ci/gitlab.bat
+  only:
+    variables:
+      - $WINDOWS == "enabled"
+
+build:base:
+  <<: *build-template
+  variables:
+    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes"
+
+# no coqide for 32bit: libgtk installation problems
+build:base+32bit:
+  <<: *build-template
+  variables:
+    OPAM_VARIANT: "+32bit"
+    COQ_EXTRA_CONF: "-native-compiler yes"
+
+build:edge:
+  <<: *build-template
+  variables:
+    OPAM_SWITCH: edge
+    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
+
+build:edge+flambda:
+  <<: *build-template
+  variables:
+    OPAM_SWITCH: edge
+    OPAM_VARIANT: "+flambda"
+    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -flambda-opts "
+    COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures"
+
+windows64:
+  <<: *windows-template
+  variables:
+    ARCH: "64"
+
+windows32:
+  <<: *windows-template
+  variables:
+    ARCH: "32"
+  except:
+    - /^pr-.*$/
+
+
+pkg:nix:
+  image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git
+  stage: test
+  variables:
+    # By default we use coq.cachix.org as an extra substituter but this can be overridden
+    EXTRA_SUBSTITUTERS: https://coq.cachix.org
+    EXTRA_PUBLIC_KEYS: coq.cachix.org-1:Jgt0DwGAUo+wpxCM52k2V+E0hLoOzFPzvg94F65agtI=
+    # The following variables should not be overridden
+    GIT_STRATEGY: none
+    CACHIX_PUBLIC_KEY: cachix.cachix.org-1:eWNHQldwUO7G2VkjpnjDbWwy4KQ/HNxht7H4SSoMckM=
+    NIXOS_PUBLIC_KEY: cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
+
+  dependencies: [] # We don't need to download build artifacts
+  before_script: [] # We don't want to use the shared 'before_script'
+  script:
+    # Use current worktree as tmpdir to allow exporting artifacts in case of failure
+    - export TMPDIR=$PWD
+    # Install Cachix as documented at https://github.com/cachix/cachix
+    - nix-env -if https://github.com/cachix/cachix/tarball/master --substituters https://cachix.cachix.org --trusted-public-keys "$CACHIX_PUBLIC_KEY"
+    # We build an expression rather than a direct URL to not be dependent on
+    # the URL location; we are forced to put the public key of cache.nixos.org
+    # because there is no --extra-trusted-public-key option.
+    - nix-build -E "import (fetchTarball $CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz) {}" -K --extra-substituters "$EXTRA_SUBSTITUTERS" --trusted-public-keys "$NIXOS_PUBLIC_KEY $EXTRA_PUBLIC_KEYS" | if [ ! -z "$CACHIX_SIGNING_KEY" ]; then cachix push coq; fi
+  artifacts:
+    name: "$CI_JOB_NAME.logs"
+    when: on_failure
+    paths:
+      - nix-build-coq.drv-0/*/test-suite/logs
+
+test-suite:base:
+  <<: *test-suite-template
+  dependencies:
+    - build:base
+
+test-suite:base+32bit:
+  <<: *test-suite-template
+  dependencies:
+    - build:base+32bit
+  variables:
+    OPAM_VARIANT: "+32bit"
+
+test-suite:edge:
+  <<: *test-suite-template
+  dependencies:
+    - build:edge
+  variables:
+    OPAM_SWITCH: edge
+
+test-suite:edge+flambda:
+  <<: *test-suite-template
+  dependencies:
+    - build:edge+flambda
+  variables:
+    OPAM_SWITCH: edge
+    OPAM_VARIANT: "+flambda"
+
+validate:base:
+  <<: *validate-template
+  dependencies:
+    - build:base
+
+validate:base+32bit:
+  <<: *validate-template
+  dependencies:
+    - build:base+32bit
+  variables:
+    OPAM_VARIANT: "+32bit"
+
+validate:edge:
+  <<: *validate-template
+  dependencies:
+    - build:edge
+  variables:
+    OPAM_SWITCH: edge
+
+validate:edge+flambda:
+  <<: *validate-template
+  dependencies:
+    - build:edge+flambda
+  variables:
+    OPAM_SWITCH: edge
+    OPAM_VARIANT: "+flambda"
+
+ci-bedrock2:
+  <<: *ci-template
+
+ci-bignums:
+  <<: *ci-template
+
+ci-color:
+  <<: *ci-template-flambda
+
+ci-compcert:
+  <<: *ci-template-flambda
+
+ci-coq-dpdgraph:
+  <<: *ci-template
+
+ci-coquelicot:
+  <<: *ci-template
+
+ci-elpi:
+  <<: *ci-template
+
+ci-equations:
+  <<: *ci-template
+
+ci-fcsl-pcm:
+  <<: *ci-template
+
+ci-fiat-crypto:
+  <<: *ci-template-flambda
+
+ci-fiat-crypto-legacy:
+  <<: *ci-template-flambda
+
+ci-fiat-parsers:
+  <<: *ci-template
+
+ci-flocq:
+  <<: *ci-template
+
+ci-formal-topology:
+  <<: *ci-template-flambda
+
+ci-geocoq:
+  <<: *ci-template-flambda
+
+ci-hott:
+  <<: *ci-template
+
+ci-iris-lambda-rust:
+  <<: *ci-template-flambda
+
+ci-ltac2:
+  <<: *ci-template
+
+ci-math-comp:
+  <<: *ci-template-flambda
+
+ci-quickchick:
+  <<: *ci-template-flambda
+
+ci-mtac2:
+  <<: *ci-template
+
+ci-sf:
+  <<: *ci-template
+
+ci-unimath:
+  <<: *ci-template-flambda
+
+ci-vst:
+  <<: *ci-template-flambda
--- a/.mailmap
+++ b/.mailmap
-## Coq contributors
-##
-## This file allows joining the different accounts of a same person.
-## Cf for instance: git shortlog -nse. More details via: man git shortlog
-##
-## To avoid spam issues, we use by default a pseudo-email <login@gforge>
-## for all persons that haven't made commits with real emails
-##
-## If you're mentionned here and want to update your information,
-## either amend this file and commit it, or contact the coqdev list
-
-Jim Apple <github.public@jbapple.com>              jbapple <github.public@jbapple.com>
-Bruno Barras <bruno.barras@inria.fr>               barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Bruno Barras <bruno.barras@inria.fr>               barras-local <barras-local@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Yves Bertot <bertot@inria.fr>                      bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Frédéric Besson <frederic.besson@inria.fr>         fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Pierre Boutillier <pierre.boutillier@ens-lyon.org> pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Pierre Boutillier <pierre.boutillier@ens-lyon.org> Pierre <pierre.boutillier@ens-lyon.org>
-Pierre Boutillier <pierre.boutillier@ens-lyon.org> Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr>
-Xavier Clerc <xavier.clerc@inria.fr>               xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Xavier Clerc <xavier.clerc@inria.fr>               xclerc <xavier.clerc@inria.fr>
-Pierre Corbineau <Pierre.Corbineau@NOSPAM@imag.fr> corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Judicaël Courant <courant@gforge>                  courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Pierre Courtieu <Pierre.Courtieu@cnam.fr>          courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7>
-David Delahaye <delahaye@gforge>                   delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Maxime Dénès <mail@maximedenes.fr>                 mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Daniel De Rauglaudre <ddr@gforge>                  ddr <ddr@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Olivier Desmettre <desmettr@gforge>                desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Damien Doligez <doligez@gforge>                    doligez <doligez@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Jean-Christophe Filliâtre <Jean-Christophe.Filliatre@lri.fr> filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Jean-Christophe Filliâtre <Jean-Christophe.Filliatre@lri.fr> Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
-Julien Forest <julien.forest@ensiie.fr>            jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Julien Forest <julien.forest@ensiie.fr>            forest <jforest@mourvedre.ensiie.fr>
-Julien Forest <julien.forest@ensiie.fr>            jforest <jforest@thune>
-Julien Forest <julien.forest@ensiie.fr>            jforest <jforest@daneel.lan.home>
-Stéphane Glondu <steph@glondu.net>                 glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Stéphane Glondu <steph@glondu.net>                 Stephane Glondu <steph@glondu.net>
-Benjamin Grégoire <benjamin.gregoire@inria.fr>     Benjamin Gregoire <Benjamin.Gregoire@inria.fr>
-Benjamin Grégoire <benjamin.gregoire@inria.fr>     bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Benjamin Grégoire <benjamin.gregoire@inria.fr>     gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Jason Gross <jgross@mit.edu>                       Jason Gross <t-jagro@microsoft.com>
-Jason Gross <jgross@mit.edu>                       Jason Gross <jasongross9@gmail.com>
-Vincent Gross <vgross@gforge>                      vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Huang Guan-Shieng <huang@gforge>                   huang <huang@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Hugo Herbelin <Hugo.Herbelin@inria.fr>             herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Tom Hutchinson <thutchin@gforge>                   thutchin <thutchin@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Cezary Kaliszyk <cek@gforge>                       cek <cek@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Florent Kirchner <fkirchne@gforge>                 fkirchne <fkirchne@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Florent Kirchner <fkirchne@gforge>                 kirchner <kirchner@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Marc Lasson <marc.lasson@gmail.com>                mlasson <marc.lasson@gmail.com>
-Pierre Letouzey <pierre.letouzey@inria.fr>         letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Assia Mahboubi <assia.mahboubi@inria.fr>           amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Evgeny Makarov <emakarov@gforge>                   emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Gregory Malecha <gmalecha@eecs.harvard.edu>        Gregory Malecha <gmalecha@cs.harvard.edu>
-Gregory Malecha <gmalecha@eecs.harvard.edu>        Gregory Malecha <gmalecha@gmail.com>
-Lionel Elie Mamane <lmamane@gforge>                lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Claude Marché <marche@gforge>                      marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Micaela Mayero <mayero@gforge>                     mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Guillaume Melquiond <guillaume.melquiond@inria.fr> gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Alexandre Miquel <miquel@gforge>                   miquel <miquel@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Benjamin Monate <monate@gforge>                    monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Julien Narboux <jnarboux@gforge>                   jnarboux <jnarboux@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Julien Narboux <jnarboux@gforge>                   narboux <narboux@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Jean-Marc Notin <notin@gforge>                     notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty <notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Jean-Marc Notin <notin@gforge>                     notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Russel O'Connor <roconnor@gforge>                  roconnor <roconnor@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Christine Paulin <cpaulin@gforge>                  cpaulin <cpaulin@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Christine Paulin <cpaulin@gforge>                  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Loïc Pottier <pottier@gforge>                      pottier <pottier@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Matthias Puech <puech@gforge>                      puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr>  regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr>
-Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel De Rauglaudre <ddr@gforge>
-Clément Renard <clrenard@gforge>                   clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Claudio Sacerdoti Coen <sacerdot@gforge>           sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Vincent Siles <vsiles@gforge>                      vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Elie Soubiran <soubiran@gforge>                    soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Matthieu Sozeau <mattam@mattam.org>                msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Matthieu Sozeau <mattam@mattam.org>                Matthieu Sozeau <matthieu.sozeau@inria.fr>
-Arnaud Spiwack <arnaud@spiwack.net>                aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Enrico Tassi <Enrico.Tassi@inria.fr>               gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Enrico Tassi <Enrico.Tassi@inria.fr>               Enrico Tassi <enrico.tassi@inria.fr>
-Enrico Tassi <Enrico.Tassi@inria.fr>               Enrico Tassi <gares@fettunta.org>
-Laurent Théry <laurent.thery@inria.fr>             thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7>
-Laurent Théry <laurent.thery@inria.fr>             thery <thery@sophia.inria.fr>
-Benjamin Werner <werner@gforge>                    werner <werner@85f007b7-540e-0410-9357-904b9bb8a0f7>
-
-# Anonymous accounts
-
-anonymous < >                                      coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>
-anonymous < >                                      (no author) <(no author)@85f007b7-540e-0410-9357-904b9bb8a0f7>
-anonymous < >                                      serpyc <serpyc@85f007b7-540e-0410-9357-904b9bb8a0f7>
--- a/.merlin
+++ b/.merlin
-FLG -rectypes -thread
+FLG -rectypes -thread -safe-string -w +a-4-9-27-41-42-44-45-48-50

+S clib
+B clib
 S config
 B config
-S ide
-B ide
 S lib
 B lib
-S intf
-B intf
 S kernel
 B kernel
 S kernel/byterun
 B kernel/byterun
+S intf
+B intf
 S library
 B library
 S engine
@@ -30,8 +30,16 @@ S parsing
 B parsing
 S stm
 B stm
+S vernac
+B vernac
 S toplevel
 B toplevel
+S plugins/ltac
+B plugins/ltac
+S API
+B API
+S ide
+B ide

 S tools
 B tools
@@ -40,4 +48,7 @@ B tools/coqdoc
 S dev
 B dev

-PKG threads.posix
+S plugins/**
+B plugins/**
+
+PKG threads.posix camlp5
--- a/.travis.yml
+++ b/.travis.yml
+dist: trusty
+
+# Travis builds are slower using sudo: false (the container-based
+# infrastructure) as of March 2017; see
+# https://github.com/coq/coq/pull/467 for some discussion.
+sudo: required
+
+# Until Ocaml becomes a language, we set a known one.
+language: c
+
+cache:
+  apt: true
+  directories:
+  - $HOME/.opam
+
+before_cache:
+  - rm -rf ~/.opam/log/
+
+addons:
+  apt:
+    sources:
+    - avsm
+## Due to issues like
+## https://github.com/travis-ci/travis-ci/issues/8507 ,
+## https://github.com/travis-ci/travis-ci/issues/9000 ,
+## https://github.com/travis-ci/travis-ci/issues/9081 , and
+## https://github.com/travis-ci/travis-ci/issues/9126 , we get frequent
+## failures with using `packages`.  Therefore, for most targets, we
+## instead invoke `apt-get update` manually with `travis_retry` before
+## invoking `apt-get install`, manually, below in the `install:`
+## target.
+#    packages:
+#    - opam
+#    - aspcud
+#    - gcc-multilib
+
+env:
+  global:
+  - NJOBS=2
+  # system is == 4.02.3
+  - COMPILER="system"
+  - COMPILER_BE="4.07.0"
+  - DUNE_VER=".1.0.0"
+  - CAMLP5_VER=".6.14"
+  - CAMLP5_VER_BE=".7.06"
+  - FINDLIB_VER=".1.4.1"
+  - FINDLIB_VER_BE=".1.8.0"
+  - LABLGTK="lablgtk.2.18.3 conf-gtksourceview.2"
+  - LABLGTK_BE="lablgtk.2.18.6 conf-gtksourceview.2"
+  - NATIVE_COMP="yes"
+  - COQ_DEST="-local"
+  - MAIN_TARGET="world"
+
+matrix:
+
+  include:
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="validate"                           TW="travis_wait"
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="validate"   COMPILER="4.02.3+32bit" TW="travis_wait"
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="validate"   COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}"
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="ci-coquelicot"
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="ci-equations"
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="ci-flocq"
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="ci-hott"
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="ci-ltac2"
+
+    - env:
+      - TEST_TARGET="lint"
+      install: []
+      before_script: []
+      addons:
+      apt:
+        sources: []
+        packages: []
+      script:
+        - dev/lint-repository.sh
+
+    # Full Coq test-suite with two compilers
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="sphinx test-suite"
+      - EXTRA_CONF="-coqide opt"
+      - EXTRA_OPAM="hevea ${LABLGTK}"
+      before_install: &sphinx-install
+      - sudo pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex
+      addons:
+        apt:
+          sources:
+          - avsm
+          packages: &extra-packages
+          - opam
+          - aspcud
+          - libgtk2.0-dev
+          - libgtksourceview2.0-dev
+          - python3
+          - python3-pip
+          - python3-setuptools
+
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="sphinx test-suite"
+      - COMPILER="${COMPILER_BE}"
+      - FINDLIB_VER="${FINDLIB_VER_BE}"
+      - CAMLP5_VER="${CAMLP5_VER_BE}"
+      - EXTRA_CONF="-coqide opt"
+      - EXTRA_OPAM="hevea ${LABLGTK_BE}"
+      before_install: *sphinx-install
+      addons:
+        apt:
+          sources:
+          - avsm
+          packages: *extra-packages
+
+    # Full test-suite with flambda
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="sphinx test-suite"
+      - COMPILER="${COMPILER_BE}+flambda"
+      - FINDLIB_VER="${FINDLIB_VER_BE}"
+      - CAMLP5_VER="${CAMLP5_VER_BE}"
+      - EXTRA_CONF="-coqide opt -flambda-opts -O3"
+      - EXTRA_OPAM="hevea ${LABLGTK_BE}"
+      before_install: *sphinx-install
+      addons:
+        apt:
+          sources:
+          - avsm
+          packages: *extra-packages
+
+    - os: osx
+      env:
+      - TEST_TARGET="test-suite"
+      - COMPILER="${COMPILER_BE}"
+      - FINDLIB_VER="${FINDLIB_VER_BE}"
+      - CAMLP5_VER="${CAMLP5_VER_BE}"
+      - NATIVE_COMP="no"
+      - COQ_DEST="-local"
+      before_install:
+      - brew update
+      - brew unlink python
+      - brew install gnu-time
+      # only way to continue using OPAM 1.2
+      - brew install https://raw.githubusercontent.com/Homebrew/homebrew-core/d156edeeed7291f4bc1e08620b331bbd05d52b78/Formula/opam.rb
+
+    - if: NOT (type = pull_request)
+      os: osx
+      osx_image: xcode7.3
+      env:
+      - TEST_TARGET=""
+      - COMPILER="${COMPILER_BE}"
+      - FINDLIB_VER="${FINDLIB_VER_BE}"
+      - CAMLP5_VER="${CAMLP5_VER_BE}"
+      - NATIVE_COMP="no"
+      - COQ_DEST="-prefix ${PWD}/_install"
+      - EXTRA_CONF="-coqide opt -warn-error yes"
+      - EXTRA_OPAM="${LABLGTK_BE}"
+      before_install:
+      - brew update
+      - brew unlink python
+      - brew install gnu-time gtk+ expat gtksourceview gdk-pixbuf
+      # only way to continue using OPAM 1.2
+      - brew install https://raw.githubusercontent.com/Homebrew/homebrew-core/d156edeeed7291f4bc1e08620b331bbd05d52b78/Formula/opam.rb
+      - brew unlink python@2
+      - brew install python3
+      - pip3 install macpack
+      before_deploy:
+        - dev/build/osx/make-macos-dmg.sh
+      deploy:
+      - provider: bintray
+        user: maximedenes
+        file: .bintray.json
+        key:
+          secure: "gUvXWwWR0gicDqsKOnBfe45taToSFied6gN8tCa5IOtl6E6gFoHoPZ83ZWXQsZP50oMDFS5eji0VQAFGEbOsGrTZaD9Y9Jnu34NND78SWL1tsJ6nHO3aCAoMpB0N3+oRuF6S+9HStU6KXWqgj+GeU4vZ4TOlG01RGctJa6U3vII="
+        skip_cleanup: true
+        on:
+          all_branches: true
+
+before_install:
+- if [ "${TRAVIS_PULL_REQUEST}" != "false" ]; then echo "Tested commit (followed by parent commits):"; git log -1; for commit in `git log -1 --format="%P"`; do echo; git log -1 $commit; done; fi
+
+install:
+- if [ "${TRAVIS_OS_NAME}" == "linux" ]; then travis_retry ./dev/tools/sudo-apt-get-update.sh -q; fi
+- if [ "${TRAVIS_OS_NAME}" == "linux" ]; then sudo apt-get install -y opam aspcud gcc-multilib --allow-unauthenticated; fi
+- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
+- opam switch "$COMPILER" && opam update
+- eval $(opam config env)
+- opam config list
+- opam install -j ${NJOBS} -y num ocamlfind${FINDLIB_VER} camlp5${CAMLP5_VER} ${EXTRA_OPAM}
+- opam list
+
+script:
+
+- set -e
+- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
+- ./configure ${COQ_DEST} -warn-error yes -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
+- echo -en 'travis_fold:end:coq.config\\r'
+
+- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
+- make -j ${NJOBS} ${MAIN_TARGET}
+- echo -en 'travis_fold:end:coq.build\\r'
+
+- echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r'
+- if [ -n "${TEST_TARGET}" ]; then ${TW} make -j ${NJOBS} ${TEST_TARGET}; fi
+- echo -en 'travis_fold:end:coq.test\\r'
+- set +e
+
+# Testing Gitter webhook
+notifications:
+  webhooks:
+    urls:
+      - https://webhooks.gitter.im/e/3cdabdec318214c7cd63
+    on_success: change  # options: [always|never|change] default: always
+    on_failure: always  # options: [always|never|change] default: always
+    on_start: never     # options: [always|never|change] default: always
--- a/CHANGES
+++ b/CHANGES
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
+# Contributing to Coq
+
+Thank you for your interest in contributing to Coq! There are many ways to contribute, and we appreciate all of them.
+
+## Bug Reports
+
+Bug reports are enormously useful to identify issues with Coq; we can't fix what we don't know about. To report a bug, please open an issue in the [Coq issue tracker](https://github.com/coq/coq/issues) (you'll need a GitHub account). You can file a bug for any of the following:
+
+- An anomaly. These are always considered bugs, so Coq will even ask you to file a bug report!
+- An error you didn't expect. If you're not sure whether it's a bug or intentional, feel free to file a bug anyway. We may want to improve the documentation or error message.
+- Missing documentation. It's helpful to track where the documentation should be improved, so please file a bug if you can't find or don't understand some bit of documentation.
+- An error message that wasn't as helpful as you'd like. Bonus points for suggesting what information would have helped you.
+- Bugs in CoqIDE should also be filed in the [Coq issue tracker](https://github.com/coq/coq/issues). Bugs in the Emacs plugin should be filed against [ProofGeneral](https://github.com/ProofGeneral/PG/issues), or against [company-coq](https://github.com/cpitclaudel/company-coq/issues) if they are specific to company-coq features.
+
+It would help if you search the existing issues before reporting a bug. This can be difficult, so consider it extra credit. We don't mind duplicate bug reports.
+
+When it applies, it's extremely helpful for bug reports to include sample code, and much better if the code is self-contained and complete. It's not necessary to minimize your bug or identify precisely where the issue is, since someone else can often do this if you include a complete example. We tend to include the code in the bug description itself, but if you have a very large input file then you can add it as an attachment.
+
+If you want to minimize your bug (or help minimize someone else's) for more extra credit, then you can use the [Coq bug minimizer](https://github.com/JasonGross/coq-tools) (specifically, the bug minimizer is the `find-bug.py` script in that repo).
+
+## Pull requests
+
+If you want to contribute a bug fix or feature yourself, pull requests on the [GitHub repository](https://github.com/coq/coq) are the way to contribute directly to the Coq implementation. We recommend you create a fork of the repository on GitHub and push your changes to a new "topic branch" in that fork. From there you can follow the [GitHub pull request documentation](https://help.github.com/articles/about-pull-requests/) to get your changes reviewed and pulled into the Coq source repository.
+
+Documentation for getting started with the Coq sources is located in various files in [`dev/doc`](/dev/doc) (for example, [debugging.md](/dev/doc/debugging.md)). For further help with the Coq sources, feel free to join the [Coq Gitter chat](https://gitter.im/coq/coq) and ask questions.
+
+Please make pull requests against the `master` branch.
+
+If it's your first significant contribution to Coq (significant means: more than fixing a typo), your pull request should include a commit adding your name to the [`CREDITS`](/CREDITS) file (possibly with the name of your institution / employer if relevant to your contribution, an ORCID if you have one —you may log into https://orcid.org/ using your institutional account to get one—, and the year of your contribution).
+
+It's helpful to run the Coq test suite with `make test-suite` before submitting your change. Travis CI runs this test suite and a much larger one including external Coq developments on every pull request, but these results take significantly longer to come back (on the order of a few hours). Running the test suite locally will take somewhere around 10-15 minutes. Refer to [`dev/ci/README.md`](/dev/ci/README.md#information-for-developers) for more information on Travis CI tests.
+
+If your pull request fixes a bug, please consider adding a regression test as well. See [`test-suite/README.md`](/test-suite/README.md) for how to do so.
+
+Don't be alarmed if the pull request process takes some time. It can take a few days to get feedback, approval on the final changes, and then a merge. Coq doesn't release new versions very frequently so it can take a few months for your change to land in a released version. That said, you can start using the latest Coq `master` branch to take advantage of all the new features, improvements, and fixes.
+
+Whitespace discipline (do not indent using tabs, no trailing spaces, text files end with newlines) is checked by Travis (using `git diff --check`). We ship a [`dev/tools/pre-commit`](/dev/tools/pre-commit) git hook which fixes these errors at commit time. `configure` automatically sets you up to use it, unless you already have a hook at `.git/hooks/pre-commit`.
+
+Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests.
+
+- [needs: rebase](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22%20) indicates the PR should be rebased on top of the latest `master` branch. See the [GitHub documentation](https://help.github.com/articles/about-git-rebase/) for a brief introduction to using `git rebase`.
+- [needs: fixing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+fixing%22) indicates the PR needs a fix, as discussed in the comments.
+- [needs: testing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22) indicates the PR needs testing. This is often used when testing beyond what the test suite can handle is required. For example, performance benchmarking is currently performed with a different infrastructure. Unless some followup is specifically requested you aren't expected to do this additional testing.
+
+The release manager uses the following filter to know which PRs seem ready for merge. If you are waiting for a PR to be merged, make sure it appears in this list:
+
+- [Pull requests ready for merge](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Apr%20is%3Aopen%20-label%3A%22needs%3A%20discussion%22%20-label%3A%22needs%3A%20testing%22%20-label%3A%22needs%3A%20fixing%22%20-label%3A%22needs%3A%20progress%22%20-label%3A%22needs%3A%20rebase%22%20-label%3A%22needs%3A%20review%22%20-label%3A%22needs%3A%20help%22%20-label%3A%22needs%3A%20independent%20fix%22%20-label%3A%22needs%3A%20feedback%22%20-label%3A%22help%20wanted%22%20-review%3Achanges_requested%20-status%3Apending%20base%3Amaster%20sort%3Aupdated-asc%20-label%3A%22needs%3A%20squashing%22%20)
+
+## Documentation
+
+Currently the process for contributing to the documentation is the same as for changing anything else in Coq, so please submit a pull request as described above.
+
+Our issue tracker includes a flag to mark bugs related to documentation. You can view a list of documentation-related bugs using a [GitHub issue search](https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+label%3A%22kind%3A+documentation%22). Many of these bugs can be fixed by contributing writing, without knowledge of Coq's OCaml source code.
+
+The sources for the [Coq reference manual](https://coq.inria.fr/distrib/current/refman/) are at [`doc/refman`](/doc/refman). These are written in LaTeX and compiled to HTML with [HeVeA](http://hevea.inria.fr/).
+
+You may also contribute to the informal documentation available in [Cocorico](https://github.com/coq/coq/wiki) (the Coq wiki), and the [Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ). Both of these are editable by anyone with a GitHub account.
+
+## Contributing outside this repository
+
+There are many useful ways to contribute to the Coq ecosystem that don't involve the Coq repository.
+
+Tutorials to teach Coq, and especially to teach particular advanced features, would be much appreciated. Some tutorials are listed on the [Coq website](https://coq.inria.fr/documentation). If you would like to add a link to this list, please make a pull request against the Coq website repository at https://github.com/coq/www.
+
+External plugins / libraries contribute to create a successful ecosystem around Coq. If your external development is mature enough, you may consider submitting it for addition to our CI tests. Refer to [`dev/ci/README.md`](/dev/ci/README.md) for more information.
+
+Ask and answer questions on [Stack Exchange](https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites) which has a helpful community of Coq users.
+
+Hang out on the Coq IRC channel, `irc://irc.freenode.net/#coq`, and help answer questions.
--- a/COPYRIGHT
+++ b/COPYRIGHT
-                     The Coq proof assistant
-
-Copyright 1999-2016 The Coq development team, INRIA, CNRS, University
-Paris Sud, University Paris 7, Ecole Polytechnique.
-
-This product includes also software developed by
-  Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega)
-  Pierre Courtieu and Julien Forest, CNAM (plugins/funind)
-  Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml)
-  Pierre Corbineau, Radboud University, Nijmegen (declarative mode)
-  John Harrison, University of Cambridge (csdp wrapper)
-  Georges Gonthier, Microsoft Research - Inria Joint Centre (plugins/ssrmatching)
-
-The file CREDITS contains a list of contributors.
-The credits section in the Reference Manual details contributions.
--- a/CREDITS
+++ b/CREDITS
 The "Coq proof assistant" was jointly developed by
- INRIA Formel, Coq, LogiCal, ProVal, TypiCal, Marelle, pi.r2 projects
-  (starting 1985),
+- INRIA Formel, Coq, LogiCal, ProVal, TypiCal, Marelle,
+  pi.r2, Ascola, Galinette projects (starting 1985),
 - Laboratoire de l'Informatique du Parallelisme (LIP)
  associated to CNRS and ENS Lyon (Sep. 1989 to Aug. 1997),
 - Laboratoire de Recherche en Informatique (LRI)
  associated to CNRS and university Paris Sud (since Sep. 1997),
 - Laboratoire d'Informatique de l'Ecole Polytechnique (LIX)
  associated to CNRS and Ecole Polytechnique (since Jan. 2003).
- Laboratoire PPS associated to CNRS and university Paris 7 (since Jan. 2009).
+- Laboratoire PPS associated to CNRS and University Paris Diderot
+  (Jan. 2009 - Dec. 2015 when it was merged into IRIF).
+- Institut de Recherche en Informatique Fondamentale (IRIF),
+  associated to CNRS and University Paris Diderot (since Jan. 2016).

 All files of the "Coq proof assistant" in directories or sub-directories of

@@ -15,8 +18,8 @@ All files of the "Coq proof assistant" in directories or sub-directories of
  scripts states tactics test-suite theories tools toplevel

 are distributed under the terms of the GNU Lesser General Public License
-Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2010,
-The Coq development team, CNRS, INRIA and Université Paris Sud.
+Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2017,
+The Coq development team, INRIA, CNRS, LIX, LRI, PPS.

 Files from the directory doc are distributed as indicated in file doc/LICENCE.

@@ -37,13 +40,18 @@ plugins/firstorder
 plugins/fourier
  developed by Loïc Pottier (INRIA-Lemme, 2001)
 plugins/funind
-  developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2008),
-  Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008)
+  developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2006-now),
+  Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008, ENSIIE, 2008-now)
  and Yves Bertot (INRIA-Marelle, 2005-2006)
-plugins/omega
-  developed by Pierre Crégut (France Telecom R&D, 1996)
+plugins/micromega
+  developed by Frédéric Besson (IRISA/INRIA, 2006-now), with some
+  extensions by Evgeny Makarov (INRIA, 2007); sum-of-squares solver and
+  interface to the csdp solver uses code from John Harrison (University
+  of Cambridge, 1998)
 plugins/nsatz
  developed by Loïc Pottier (INRIA-Marelle, 2009-2011)
+plugins/omega
+  developed by Pierre Crégut (France Telecom R&D, 1996)
 plugins/quote
  developed by Patrick Loiseleur (LRI, 1997-1999)
 plugins/romega
@@ -54,16 +62,14 @@ plugins/setoid_ring
  developed by Benjamin Grégoire (INRIA-Everest, 2005-2006),
  Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006)
  and Bruno Barras (INRIA LogiCal, 2005-2006),
+plugins/ssreflect
+  developed by Georges Gonthier (Microsoft Research - Inria Joint Centre, 2007-2011),
+  Assia Mahboubi and Enrico Tassi (Inria, 2011-now).
 plugins/ssrmatching
  developed by Georges Gonthier (Microsoft Research - Inria Joint Centre, 2007-2011),
  and Enrico Tassi (Inria-Marelle, 2011-now)
 plugins/subtac
  developed by Matthieu Sozeau (LRI, 2005-2008)
-plugins/micromega
-  developed by Frédéric Besson (IRISA/INRIA, 2006-2008), with some
-  extensions by Evgeny Makarov (INRIA, 2007); sum-of-squares solver and
-  interface to the csdp solver uses code from John Harrison (University
-  of Cambridge, 1998)
 theories/ZArith
  started by Pierre Crégut (France Telecom R&D, 1996)
 theories/Strings
@@ -94,32 +100,42 @@ of the Coq Proof assistant during the indicated time:

  Bruno Barras (INRIA, 1995-now)
  Yves Bertot (INRIA, 2000-now)
-  Pierre Boutillier (INRIA-PPS, 2010-now)
+  Pierre Boutillier (INRIA-PPS, 2010-2015)
  Xavier Clerc (INRIA, 2012-2014)
+  Tej Chajed (MIT, 2016-now)
  Jacek Chrzaszcz (LRI, 1998-2003)
  Thierry Coquand (INRIA, 1985-1989)
  Pierre Corbineau (LRI, 2003-2005, Nijmegen, 2005-2008, Grenoble 1, 2008-2011)
  Cristina Cornes (INRIA, 1993-1996)
  Yann Coscoy (INRIA Sophia-Antipolis, 1995-1996)
+  Pierre Courtieu (CNAM, 2006-now)
  David Delahaye (INRIA, 1997-2002)
  Maxime Dénès (INRIA, 2013-now)
-  Daniel de Rauglaudre (INRIA, 1996-1998)
+  Daniel de Rauglaudre (INRIA, 1996-1998, 2012, 2016)
  Olivier Desmettre (INRIA, 2001-2003)
  Gilles Dowek (INRIA, 1991-1994)
  Amy Felty (INRIA, 1993)
  Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, LRI, 1997-2008)
+  Emilio Jesús Gallego Arias (MINES ParisTech 2015-now)
+  Gaetan Gilbert (INRIA-Galinette, 2016-now)
  Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998)
  Stéphane Glondu (INRIA-PPS, 2007-2013)
  Benjamin Grégoire (INRIA, 2003-2011)
+  Jason Gross (MIT 2013-now)
  Hugo Herbelin (INRIA, 1996-now)
  Sébastien Hinderer (INRIA, 2014)
  Gérard Huet (INRIA, 1985-1997)
-  Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, INRIA-PPS, 2009-now)
+  Matej Košík (INRIA, 2015-2017)
+  Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008,
+                   INRIA-PPS then IRIF, 2009-now)
  Patrick Loiseleur (Paris Sud, 1997-1999)
  Evgeny Makarov (INRIA, 2007)
+  Gregory Malecha (Harvard University 2013-2015,
+                   University of California, San Diego 2016)
+  Cyprien Mangin (INRIA-PPS then IRIF, 2015-now)
  Pascal Manoury (INRIA, 1993)
-  Micaela Mayero (INRIA, 1997-2002)
  Claude Marché (INRIA, 2003-2004 & LRI, 2004)
+  Micaela Mayero (INRIA, 1997-2002)
  Guillaume Melquiond (INRIA, 2009-now)
  Benjamin Monate (LRI, 2003)
  César Muñoz (INRIA, 1994-1995)
@@ -129,18 +145,28 @@ of the Coq Proof assistant during the indicated time:
  Catherine Parent-Vigouroux (ENS Lyon, 1992-1995)
  Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997,
                            LRI, 1997-2006)
-  Pierre-Marie Pédrot (INRIA-PPS, 2011-now)
+  Pierre-Marie Pédrot (INRIA-PPS, 2011-2015, INRIA-Ascola, 2015-2016,
+                       University of Ljubljana, 2016-2017,
+                       MPI-SWS, 2017-2018)
+  Clément Pit-Claudel (MIT, 2015-2018)
  Matthias Puech (INRIA-Bologna, 2008-2011)
-  Yann Régis-Gianas (INRIA-PPS, 2009-now)
+  Yann Régis-Gianas (INRIA-PPS then IRIF, 2009-now)
  Clément Renard (INRIA, 2001-2004)
  Claudio Sacerdoti Coen (INRIA, 2004-2005)
  Amokrane Saïbi (INRIA, 1993-1998)
  Vincent Siles (INRIA, 2007)
  Élie Soubiran (INRIA, 2007-2010)
  Matthieu Sozeau (INRIA, 2005-now)
-  Arnaud Spiwack (INRIA, 2006-now)
+  Arnaud Spiwack (INRIA-LIX-Chalmers University, 2006-2010,
+                  INRIA, 2011-2014, MINES ParisTech 2014-2015,
+                  Tweag/IO 2015-now)
+  Paul Steckler (MIT 2016-2018)
  Enrico Tassi (INRIA, 2011-now)
+  Amin Timany (Katholieke Universiteit Leuven, 2017)
  Benjamin Werner (INRIA, 1989-1994)
+  Nickolai Zeldovich (MIT 2014-2016)
+  Théo Zimmermann (ORCID: https://orcid.org/0000-0002-3580-8806,
+                   INRIA-PPS then IRIF, 2015-now)

 ***************************************************************************
 INRIA refers to:

--- a/INSTALL
+++ b/INSTALL

-            INSTALLATION PROCEDURES FOR THE COQ V8.6 SYSTEM
-            -----------------------------------------------
+            INSTALLATION PROCEDURE
+            ----------------------


 WHAT DO YOU NEED ?
@@ -27,27 +27,52 @@ WHAT DO YOU NEED ?

     port install coq

-   To compile Coq V8.6 yourself, you need:
+   To compile Coq yourself, you need:

-   - Objective Caml version 4.01.0 or later
-     (available at http://caml.inria.fr/)
+   - OCaml (version >= 4.02.3)
+     (available at https://ocaml.org/)
+     (This version of Coq has been tested up to OCaml 4.07.0)

-   - Findlib (included in OCaml binary distribution under windows,
-     probably available in your distribution and for sure at
-     http://projects.camlcity.org/projects/findlib.html)
+   - The Num package, which used to be part of the OCaml standard library,
+     if you are using an OCaml version >= 4.06.0

-   - Camlp5 (version >= 6.02) (Coq compiles with Camlp4 but might be
-     less well supported, for instance, Objective Caml version 4.02.1
-     is then needed or a patched version of 4.01.0 as e.g. version
-     4.01.0-4 in Debian Jessie)
+   - Findlib (version >= 1.4.1)
+     (available at http://projects.camlcity.org/projects/findlib.html)
+
+   - Camlp5 (version >= 6.14)
+     (available at https://camlp5.github.io/)

   - GNU Make version 3.81 or later

   - a C compiler

   - for Coqide, the Lablgtk development files, and the GTK libraries
-     incuding gtksourceview, see INSTALL.ide for more details
+     including gtksourceview, see INSTALL.ide for more details
+
+   Note that num, camlp5 and lablgtk should be properly registered with
+   findlib/ocamlfind as Coq's makefile will use it to locate the
+   libraries during the build.
+
+   Opam (https://opam.ocaml.org/) is recommended to install OCaml and
+   the corresponding packages.
+
+   $ opam install num ocamlfind camlp5 lablgtk conf-gtksourceview
+
+   should get you a reasonable OCaml environment to compile Coq.
+
+   Nix users can also get all the required dependencies by running:

+   $ nix-shell
+
+   Advanced users may want to experiment with the OCaml Flambda
+   compiler as way to improve the performance of Coq. In order to
+   profit from Flambda, a special build of the OCaml compiler that has
+   the Flambda optimizer enabled must be installed. For OPAM users,
+   this amounts to installing a compiler switch ending in `+flambda`,
+   such as `4.07.0+flambda`. For other users, YMMV. Once `ocamlopt
+   -config` reports that Flambda is available, some further
+   optimization options can be used; see the entry about -flambda-opts
+   below for more details.

 QUICK INSTALLATION PROCEDURE.
 =============================
@@ -55,29 +80,26 @@ QUICK INSTALLATION PROCEDURE.
 1. ./configure
 2. make
 3. make install (you may need superuser rights)
-4. make clean
-

 INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 =================================================

-1- Check that you have the Objective Caml compiler installed on your
+1- Check that you have the OCaml compiler installed on your
   computer and that "ocamlc" (or, better, its native code version
   "ocamlc.opt") lies in a directory which is present in your $PATH
   environment variable. At the time of writing this sentence, all
-   versions of Objective Caml later or equal to 4.01.0 are
-   supported to the exception of Objective Caml 4.02.0.
+   versions of Objective Caml later or equal to 4.02.3 are
+   supported.

   To get Coq in native-code, (it runs 4 to 10 times faster than
   bytecode, but it takes more time to get compiled and the binary is
   bigger), you will also need the "ocamlopt" (or its native code version
   "ocamlopt.opt") command.

-2- Check that you have Camlp5 (or a supported Camlp4) installed on your
-   computer and that the command "camlp5" lies in a directory which
-   is present in your $PATH environment variable path.
-   (You need Camlp5/4 in both bytecode and native versions if
-   your platform supports it).
+2- Check that you have Camlp5 installed on your computer and that the
+   command "camlp5" lies in a directory which is present in your $PATH
+   environment variable path.  (You need Camlp5 in both bytecode and
+   native versions if your platform supports it).

 3- The uncompression and un-tarring of the distribution file gave birth
   to a directory named "coq-8.xx". You can rename this directory and put
@@ -128,14 +150,38 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 	Use <command> to open an URL in a browser. %s must appear in <command>,
 	and will be replaced by the URL.

+-flambda-opts <flags>
+        This experimental option will pass specific user flags to the
+        OCaml optimizing compiler. In most cases, this option is used
+        to tweak the flambda backend; for maximum performance we
+        recommend using
+
+        -flambda-opts `-O3 -unbox-closures`
+
+        but of course you are free to try with a different combination
+        of flags. You can read more at
+        https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html
+
+        There is a known problem with certain OCaml versions and
+        `native_compute`, that will make compilation to require
+        a large amount of RAM (>= 10GiB) in some particular files.
+
+        We recommend disabling native compilation (`-native-compiler no`)
+        with flambda unless you use OCaml >= 4.07.0.
+
+        c.f. https://caml.inria.fr/mantis/view.php?id=7630
+
 5- Still in the root directory, do

 	make

-   to compile Coq in Objective Caml bytecode (and native-code if supported).
+   to compile Coq in the best OCaml mode available (native-code if supported,
+   bytecode otherwise).

   This will compile the entire system. This phase can take more or less time,
-   depending on your architecture and is fairly verbose.
+   depending on your architecture and is fairly verbose. On a multi-core machine,
+   it is recommended to compile in parallel, via make -jN where N is your number
+   of cores.

 6- You can now install the Coq system. Executables, libraries, manual pages
   and emacs mode are copied in some standard places of your system, defined at
@@ -145,13 +191,20 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
       	make install

   Of course, you may need superuser rights to do that.
-   To use the Coq emacs mode you also need to put the following lines
-   in you .emacs file:

-        (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
-        (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)
+7- Optionally, you could build the bytecode version of Coq via:
+
+        make byte
+
+   and install it via

-7- You can now clean all the sources. (You can even erase them.)
+        make install-byte
+
+  This version is quite slower than the native code version of Coq, but could
+  be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml
+  toplevel accessible via the Drop command.
+
+8- You can now clean all the sources. (You can even erase them.)

 	make clean

@@ -169,16 +222,10 @@ INSTALLATION PROCEDURE FOR ADVANCED USERS.
   Then compile the sources as described in step 5 above. The resulting
   binaries will reside in the subdirectory bin/.

-   If you want to compile the sources for debugging (i.e. with the option
-   -g of the Caml compiler) then add the -debug option at configuration
-   step :
-
-	./configure -debug <other options>
-
-   and then compile the sources (step 5). Then you must make a Coq toplevel
-   including your own tactics, which must be compiled with -g, with coqmktop.
-   See the chapter 16 of the Coq Reference Manual for details about how
-   to use coqmktop and the Objective Caml debugger with Coq.
+   Unless you pass the -nodebug option to ./configure, the -g option of the
+   OCaml compiler will be used during compilation to allow debugging.
+   See the debugging file in dev/doc and the chapter 15 of the Coq Reference
+   Manual for details about how to use the OCaml debugger with Coq.


 THE AVAILABLE COMMANDS.
@@ -189,11 +236,14 @@ THE AVAILABLE COMMANDS.
 	coqtop		The Coq toplevel
 	coqc		The Coq compiler

-   Under architecture where ocamlopt is available, there are actually two
-   binaries for the interactive system, coqtop.byte and coqtop (respectively
-   bytecode and native code versions of Coq).  coqtop is a link to coqtop.byte
-   otherwise. coqc also invokes the fastest version of Coq.  Options -opt and
-   -byte to coqtop and coqc selects a particular binary.
+   Under architecture where ocamlopt is available, coqtop is the native code
+   version of Coq. On such architecture, you could additionally request
+   the build of the bytecode version of Coq via 'make byte' and install it via
+   'make install-byte'. This will create  an extra binary named coqtop.byte,
+   that could be used for debugging purpose. If native code isn't available,
+   coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte.
+   coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop
+   and coqc selects a particular binary.

    * `coqtop' launches Coq in the interactive mode. By default it loads
      basic logical definitions and tactics from the Init directory.
@@ -211,8 +261,6 @@ THE AVAILABLE COMMANDS.
   directory, or read online on http://coq.inria.fr/doc/)
   and in the corresponding manual pages.

-   There is also a tutorial and a FAQ; see http://coq.inria.fr/getting-started
-

 COMPILING FOR DIFFERENT ARCHITECTURES.
 ======================================

--- a/INSTALL.doc
+++ b/INSTALL.doc
@@ -22,25 +22,42 @@ To produce all the documents, the following tools are needed:
  - dvips
  - bibtex
  - makeindex
-  - fig2dev (transfig)
-  - convert (ImageMagick)
  - hevea
-  - hacha
+  - Python 3
+  - Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/)
+  - sphinx_rtd_theme
+  - pexpect
+  - beautifulsoup4
+  - Antlr4 runtime for Python 3


-Under Debian based operating systems (Debian, Ubuntu, ...) a
-working set of packages for compiling the documentation for Coq is:
+Under recent Debian based operating systems (Debian 10 "Buster",
+Ubuntu 18.04, ...) a working set of packages for compiling the
+documentation for Coq is:

-  texlive texlive-latex-extra texlive-math-extra texlive-fonts-extra
-  texlive-humanities texlive-pictures latex-xcolor hevea transfig
-  imagemagick
+  texlive-latex-extra texlive-fonts-recommended hevea python3-sphinx
+  python3-pexpect python3-sphinx-rtd-theme python3-bs4
+  python3-sphinxcontrib.bibtex python3-pip

+Then, install the Python3 Antlr4 package:
+
+  pip3 install antlr4-python3-runtime
+
+Nix users should get the correct development environment to build the
+Sphinx documentation from Coq's `default.nix`. [Note Nix setup doesn't
+include the LaTeX packages needed to build the full documentation.]
+
+If you are in an older/different distribution you can install the
+Python packages required to build the user manual using python3-pip:
+
+  pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex

 Compilation
 -----------

 To produce all documentation about Coq, just run:

+   ./configure            (if you hadn't already)
   make doc


@@ -55,8 +72,8 @@ Alternatively, you can use some specific targets:
   make doc-html
        to produce all html documents

-   make refman
-        to produce all formats of the reference manual
+   make sphinx
+        to produce the HTML version of the reference manual

   make tutorial
        to produce all formats of the tutorial
@@ -71,6 +88,10 @@ Alternatively, you can use some specific targets:
        to produce all formats of the Coq standard library


+Also note the "-with-doc yes" option of ./configure to enable the
+build of the documentation as part of the default make target.
+
+
 Installation
 ------------


--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -22,7 +22,7 @@ Else, read the rest of this document to compile your own CoqIde.

 COMPILATION REQUIREMENTS

- OCaml >= 4.01 with native threads support.
+- OCaml >= 4.02.3 with native threads support.
 - make world must succeed.
 - The graphical toolkit GTK+ 2.x. See http://www.gtk.org.
  The official supported version is at least 2.24.x.
@@ -39,7 +39,7 @@ COMPILATION REQUIREMENTS
  install GTK+ 2.x, should you need to force it for one reason
  or another.)
 - The OCaml bindings for GTK+ 2.x, lablgtk2 with support for gtksourceview2.
-  You need at least version 2.16.
+  You need at least version 2.18.3.

  Your distribution may contain precompiled packages. For example, for
  Debian, run
@@ -57,7 +57,7 @@ COMPILATION REQUIREMENTS
        ./configure && make world && make install

   You must have write access to the OCaml standard library path.
-   If this fails, read lablgtk-2.14.2/README.
+   If this fails, read the README.


 INSTALLATION

--- a/META.coq
+++ b/META.coq
+# TODO: Generate automatically with Dune
+
 description = "The Coq Proof Assistant Plugin API"
-version = "8.6"
+version = "8.8"

 directory = ""
 requires = "camlp5"
@@ -7,61 +9,67 @@ requires = "camlp5"
 package "config" (

  description = "Coq Configuration Variables"
-  version     = "8.6"
+  version     = "8.8"

  directory   = "config"

 )

+package "clib" (
+  description = "Base General Coq Library"
+  version     = "8.8"
+
+  directory   = "clib"
+  requires    = "num, str, unix, threads"
+
+  archive(byte)    = "clib.cma"
+  archive(native)  = "clib.cmxa"
+)
+
 package "lib" (

-  description = "Base Coq Library"
-  version     = "8.6"
+  description = "Base Coq-Specific Library"
+  version     = "8.8"

  directory   = "lib"

-  requires         = "coq.config"
+  requires    = "coq.clib, coq.config"

-  archive(byte)    = "clib.cma"
-  archive(byte)   += "lib.cma"
-
-  archive(native)  = "clib.cmxa"
-  archive(native) += "lib.cmxa"
+  archive(byte)   = "lib.cma"
+  archive(native) = "lib.cmxa"

 )

 package "vm" (

  description = "Coq VM"
+  version     = "8.8"

-  version     = "8.6"
+  directory        = "kernel/byterun"

-# EJGA FIXME: Unfortunately dllpath is dependent on the type of Coq
-# install. In a local one we'll want kernel/byterun, in a non-local
-# one we want to set it to coqlib. We should thus generate this file
-# at configure time, but let's hear for some more feedback from
-# experts.
+# We could generate this file at configure time for the share byte
+# build path to work properly.
+#
+# Enable this setting for local byte builds if you want dynamic linking:
+#
+#  linkopts(byte)   = "-dllpath path_to_coq/kernel/byterun/ -dllib -lcoqrun"

-# Enable for local native & byte builds
-#  directory        = "kernel/byterun"
+# We currently prefer static linking of the VM.
+  archive(byte)    = "libcoqrun.a"
+  linkopts(byte)   = "-custom"

-# Enable for local byte builds and set up properly
-#  linkopts(byte)   = "-dllpath /path/to/coq/kernel/byterun/ -dllib -lcoqrun"
-
-# Disable for local byte builds
-  linkopts(byte)   = "-dllib -lcoqrun"
  linkopts(native) = "-cclib -lcoqrun"

 )

 package "kernel" (

-  description = "The Coq's Kernel"
-  version     = "8.6"
+  description = "Coq's Kernel"
+  version     = "8.8"

  directory   = "kernel"

-  requires    = "coq.lib, coq.vm"
+  requires    = "dynlink, coq.lib, coq.vm"

  archive(byte)    = "kernel.cma"
  archive(native)  = "kernel.cmxa"
@@ -71,7 +79,7 @@ package "kernel" (
 package "library" (

  description = "Coq Libraries (vo) support"
-  version     = "8.6"
+  version     = "8.8"

  requires    = "coq.kernel"

@@ -85,18 +93,20 @@ package "library" (
 package "intf" (

  description = "Coq Public Data Types"
-  version     = "8.6"
+  version     = "8.8"

  requires    = "coq.library"

  directory   = "intf"

+  archive(byte)    = "intf.cma"
+  archive(native)  = "intf.cmxa"
 )

 package "engine" (

-  description = "Coq Libraries (vo) support"
-  version     = "8.6"
+  description = "Coq Tactic Engine"
+  version     = "8.8"

  requires    = "coq.library"
  directory   = "engine"
@@ -109,7 +119,7 @@ package "engine" (
 package "pretyping" (

  description = "Coq Pretyper"
-  version     = "8.6"
+  version     = "8.8"

  requires    = "coq.engine"
  directory   = "pretyping"
@@ -122,7 +132,7 @@ package "pretyping" (
 package "interp" (

  description = "Coq Term Interpretation"
-  version     = "8.6"
+  version     = "8.8"

  requires    = "coq.pretyping"
  directory   = "interp"
@@ -135,7 +145,7 @@ package "interp" (
 package "grammar" (

  description = "Coq Base Grammar"
-  version     = "8.6"
+  version     = "8.8"

  requires    = "coq.interp"
  directory   = "grammar"
@@ -147,7 +157,7 @@ package "grammar" (
 package "proofs" (

  description = "Coq Proof Engine"
-  version     = "8.6"
+  version     = "8.8"

  requires    = "coq.interp"
  directory   = "proofs"
@@ -160,9 +170,9 @@ package "proofs" (
 package "parsing" (

  description = "Coq Parsing Engine"
-  version     = "8.6"
+  version     = "8.8"

-  requires    = "coq.proofs"
+  requires    = "camlp5.gramlib, coq.proofs"
  directory   = "parsing"

  archive(byte)    = "parsing.cma"
@@ -172,8 +182,8 @@ package "parsing" (

 package "printing" (

-  description = "Coq Printing Libraries"
-  version     = "8.6"
+  description = "Coq Printing Engine"
+  version     = "8.8"

  requires    = "coq.parsing"
  directory   = "printing"
@@ -185,8 +195,8 @@ package "printing" (

 package "tactics" (

-  description = "Coq Tactics"
-  version     = "8.6"
+  description = "Coq Basic Tactics"
+  version     = "8.8"

  requires    = "coq.printing"
  directory   = "tactics"
@@ -196,12 +206,25 @@ package "tactics" (

 )

+package "vernac" (
+
+  description = "Coq Vernacular Interpreter"
+  version     = "8.8"
+
+  requires    = "coq.tactics"
+  directory   = "vernac"
+
+  archive(byte)    = "vernac.cma"
+  archive(native)  = "vernac.cmxa"
+
+)
+
 package "stm" (

  description = "Coq State Transactional Machine"
-  version     = "8.6"
+  version     = "8.8"

-  requires    = "coq.tactics"
+  requires    = "coq.vernac"
  directory   = "stm"

  archive(byte)    = "stm.cma"
@@ -212,7 +235,7 @@ package "stm" (
 package "toplevel" (

  description = "Coq Toplevel"
-  version     = "8.6"
+  version     = "8.8"

  requires    = "coq.stm"
  directory   = "toplevel"
@@ -222,28 +245,327 @@ package "toplevel" (

 )

-package "highparsing" (
+package "idetop" (

-  description = "Coq Extra Parsing"
-  version     = "8.6"
+  description = "Coq IDE Libraries"
+  version     = "8.8"

  requires    = "coq.toplevel"
-  directory   = "parsing"
+  directory   = "ide"
+
+  archive(byte)    = "coqidetop.cma"
+  archive(native)  = "coqidetop.cmxa"
+
+)

-  archive(byte)    = "highparsing.cma"
-  archive(native)  = "highparsing.cmxa"
+# XXX Depends on way less than toplevel
+package "ide" (
+
+  description = "Coq IDE Libraries"
+  version     = "8.8"
+
+# XXX Add GTK
+  requires    = "coq.toplevel"
+  directory   = "ide"
+
+  archive(byte)    = "ide.cma"
+  archive(native)  = "ide.cmxa"

 )

+package "plugins" (
+
+  description = "Coq built-in plugins"
+  version     = "8.8"
+
+  directory   = "plugins"
+
  package "ltac" (

    description = "Coq LTAC Plugin"
-  version     = "8.6"
+    version     = "8.8"

-  requires    = "coq.highparsing"
+    requires    = "coq.stm"
    directory   = "ltac"

-  archive(byte)    = "ltac.cma"
-  archive(native)  = "ltac.cmxa"
+    archive(byte)    = "ltac_plugin.cmo"
+    archive(native)  = "ltac_plugin.cmx"
+
+  )
+
+  package "tauto" (
+
+    description = "Coq tauto plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "ltac"
+
+    archive(byte)    = "tauto_plugin.cmo"
+    archive(native)  = "tauto_plugin.cmx"
+  )
+
+  package "omega" (
+
+    description = "Coq omega plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "omega"
+
+    archive(byte)    = "omega_plugin.cmo"
+    archive(native)  = "omega_plugin.cmx"
+  )
+
+  package "romega" (
+
+    description = "Coq romega plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.omega"
+    directory   = "romega"
+
+    archive(byte)    = "romega_plugin.cmo"
+    archive(native)  = "romega_plugin.cmx"
+  )
+
+  package "micromega" (
+
+    description = "Coq micromega plugin"
+    version     = "8.8"
+
+    requires    = "num,coq.plugins.ltac"
+    directory   = "micromega"
+
+    archive(byte)    = "micromega_plugin.cmo"
+    archive(native)  = "micromega_plugin.cmx"
+  )
+
+  package "quote" (
+
+    description = "Coq quote plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "quote"
+
+    archive(byte)    = "quote_plugin.cmo"
+    archive(native)  = "quote_plugin.cmx"
+  )
+
+  package "newring" (
+
+    description = "Coq newring plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.quote"
+    directory   = "setoid_ring"
+
+    archive(byte)    = "newring_plugin.cmo"
+    archive(native)  = "newring_plugin.cmx"
+  )
+
+  package "fourier" (
+
+    description = "Coq fourier plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "fourier"
+
+    archive(byte)    = "fourier_plugin.cmo"
+    archive(native)  = "fourier_plugin.cmx"
+  )
+
+  package "extraction" (
+
+    description = "Coq extraction plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "extraction"
+
+    archive(byte)    = "extraction_plugin.cmo"
+    archive(native)  = "extraction_plugin.cmx"
+  )

+  package "cc" (
+
+    description = "Coq cc plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "cc"
+
+    archive(byte)    = "cc_plugin.cmo"
+    archive(native)  = "cc_plugin.cmx"
+  )
+
+  package "ground" (
+
+    description = "Coq ground plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "firstorder"
+
+    archive(byte)    = "ground_plugin.cmo"
+    archive(native)  = "ground_plugin.cmx"
+  )
+
+  package "rtauto" (
+
+    description = "Coq rtauto plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "rtauto"
+
+    archive(byte)    = "rtauto_plugin.cmo"
+    archive(native)  = "rtauto_plugin.cmx"
+  )
+
+  package "btauto" (
+
+    description = "Coq btauto plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "btauto"
+
+    archive(byte)    = "btauto_plugin.cmo"
+    archive(native)  = "btauto_plugin.cmx"
+  )
+
+  package "recdef" (
+
+    description = "Coq recdef plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.extraction"
+    directory   = "funind"
+
+    archive(byte)    = "recdef_plugin.cmo"
+    archive(native)  = "recdef_plugin.cmx"
+  )
+
+  package "nsatz" (
+
+    description = "Coq nsatz plugin"
+    version     = "8.8"
+
+    requires    = "num,coq.plugins.ltac"
+    directory   = "nsatz"
+
+    archive(byte)    = "nsatz_plugin.cmo"
+    archive(native)  = "nsatz_plugin.cmx"
+  )
+
+  package "natsyntax" (
+
+    description = "Coq natsyntax plugin"
+    version     = "8.8"
+
+    requires    = ""
+    directory   = "syntax"
+
+    archive(byte)    = "nat_syntax_plugin.cmo"
+    archive(native)  = "nat_syntax_plugin.cmx"
+  )
+
+  package "zsyntax" (
+
+    description = "Coq zsyntax plugin"
+    version     = "8.8"
+
+    requires    = ""
+    directory   = "syntax"
+
+    archive(byte)    = "z_syntax_plugin.cmo"
+    archive(native)  = "z_syntax_plugin.cmx"
+  )
+
+  package "rsyntax" (
+
+    description = "Coq rsyntax plugin"
+    version     = "8.8"
+
+    requires    = ""
+    directory   = "syntax"
+
+    archive(byte)    = "r_syntax_plugin.cmo"
+    archive(native)  = "r_syntax_plugin.cmx"
+  )
+
+  package "int31syntax" (
+
+    description = "Coq int31syntax plugin"
+    version     = "8.8"
+
+    requires    = ""
+    directory   = "syntax"
+
+    archive(byte)    = "int31_syntax_plugin.cmo"
+    archive(native)  = "int31_syntax_plugin.cmx"
+  )
+
+  package "asciisyntax" (
+
+    description = "Coq asciisyntax plugin"
+    version     = "8.8"
+
+    requires    = ""
+    directory   = "syntax"
+
+    archive(byte)    = "ascii_syntax_plugin.cmo"
+    archive(native)  = "ascii_syntax_plugin.cmx"
+  )
+
+  package "stringsyntax" (
+
+    description = "Coq stringsyntax plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.asciisyntax"
+    directory   = "syntax"
+
+    archive(byte)    = "string_syntax_plugin.cmo"
+    archive(native)  = "string_syntax_plugin.cmx"
+  )
+
+  package "derive" (
+
+    description = "Coq derive plugin"
+    version     = "8.8"
+
+    requires    = ""
+    directory   = "derive"
+
+    archive(byte)    = "derive_plugin.cmo"
+    archive(native)  = "derive_plugin.cmx"
+  )
+
+  package "ssrmatching" (
+
+    description = "Coq ssrmatching plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "ssrmatching"
+
+    archive(byte)    = "ssrmatching_plugin.cmo"
+    archive(native)  = "ssrmatching_plugin.cmx"
+  )
+
+  package "ssreflect" (
+
+    description = "Coq ssreflect plugin"
+    version     = "8.8"
+
+    requires    = "coq.plugins.ssrmatching"
+    directory   = "ssr"
+
+    archive(byte)    = "ssreflect_plugin.cmo"
+    archive(native)  = "ssreflect_plugin.cmx"
+  )
 )
--- a/Makefile
+++ b/Makefile
-#######################################################################
-#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
-# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-osay              #
-#   \VV/  #############################################################
-#    //   #      This file is distributed under the terms of the      #
-#         #       GNU Lesser General Public License Version 2.1       #
-#######################################################################
+##########################################################################
+##         #   The Coq Proof Assistant / The Coq Development Team       ##
+##  v      #   INRIA, CNRS and contributors - Copyright 1999-2018       ##
+## <O___,, #       (see CREDITS file for the list of authors)           ##
+##   \VV/  ###############################################################
+##    //   #    This file is distributed under the terms of the         ##
+##         #     GNU Lesser General Public License Version 2.1          ##
+##         #     (see LICENSE file for the text of the license)         ##
+##########################################################################


 # Makefile for Coq
@@ -15,7 +17,7 @@
 # You won't find Makefiles in sub-directories and this is done on purpose.
 # If you are not yet convinced of the advantages of a single Makefile, please
 # read
-#    http://miller.emu.id.au/pmiller/books/rmch/
+#    http://aegis.sourceforge.net/auug97.pdf
 # before complaining.
 #
 # When you are working in a subdir, you can compile without moving to the
@@ -42,9 +44,9 @@
 # to communicate between make sub-calls (in Win32, 8kb max per env variable,
 # 32kb total)

-# !! Before using FIND_VCS_CLAUSE, please read how you should in the !!
-# !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt         !!
-FIND_VCS_CLAUSE:='(' \
+# !! Before using FIND_SKIP_DIRS, please read how you should in the !!
+# !! FIND_SKIP_DIRS section of dev/doc/build-system.dev.txt         !!
+FIND_SKIP_DIRS:='(' \
  -name '{arch}' -o \
  -name '.svn' -o \
  -name '_darcs' -o \
@@ -52,27 +54,31 @@ FIND_VCS_CLAUSE:='(' \
  -name '.bzr' -o \
  -name 'debian' -o \
  -name "$${GIT_DIR}" -o \
-  -name '_build' \
+  -name '_build' -o \
+  -name '_build_ci' -o \
+  -name '_install_ci' -o \
+  -name 'user-contrib' -o \
+  -name 'coq-makefile' -o \
+  -name '.opamcache' -o \
+  -name '.coq-native' \
 ')' -prune -o

 define find
- $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||')
+ $(shell find . $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||')
 endef

 define findindir
- $(shell find $(1) $(FIND_VCS_CLAUSE) '(' -name $(2) ')' -print | sed 's|^\./||')
-endef
-
-define findx
- $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -exec $(2) {} \; | sed 's|^\./||')
+ $(shell find $(1) $(FIND_SKIP_DIRS) '(' -name $(2) ')' -print | sed 's|^\./||')
 endef

 ## Files in the source tree

 LEXFILES := $(call find, '*.mll')
-export MLLIBFILES := $(call find, '*.mllib') $(call find, '*.mlpack')
+export MLLIBFILES := $(call find, '*.mllib')
+export MLPACKFILES := $(call find, '*.mlpack')
 export ML4FILES := $(call find, '*.ml4')
 export CFILES := $(call findindir, 'kernel/byterun', '*.c')
+export MERLINFILES := $(call find, '.merlin')

 # NB: The lists of currently existing .ml and .mli files will change
 # before and after a build or a make clean. Hence we do not export
@@ -84,10 +90,9 @@ EXISTINGMLI := $(call find, '*.mli')
 ## Files that will be generated

 GENML4FILES:= $(ML4FILES:.ml4=.ml)
-export GENMLFILES:=$(LEXFILES:.mll=.ml) tools/tolink.ml kernel/copcodes.ml
+export GENMLFILES:=$(LEXFILES:.mll=.ml) kernel/copcodes.ml
 export GENHFILES:=kernel/byterun/coq_jumptbl.h
-export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
-export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES)
+export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)

 # NB: all files in $(GENFILES) can be created initially, while
 # .ml files in $(GENML4FILES) might need some intermediate building.
@@ -95,11 +100,7 @@ export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES)

 ## More complex file lists

-define diff
- $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
-endef
-
-export MLSTATICFILES := $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES))
+export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES), $(EXISTINGML))
 export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))

 include Makefile.common
@@ -113,16 +114,19 @@ NOARG: world
 .PHONY: NOARG help noconfig submake

 help:
-	@echo "Please use either"
+	@echo "Please use either:"
 	@echo "   ./configure"
 	@echo "   make world"
 	@echo "   make install"
 	@echo "   make clean"
 	@echo "or make archclean"
-	@echo
 	@echo "For make to be verbose, add VERBOSE=1"
+	@echo "If you want camlp5 to generate human-readable files, add READABLE_ML4=1"
 	@echo
-	@echo "If you want camlp{4,5} to generate human-readable files, add READABLE_ML4=1"
+	@echo "Bytecode compilation is now a separate target:"
+	@echo "   make byte"
+	@echo "   make install-byte"
+	@echo "Please do not mix bytecode and native targets in the same make -j"

 UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?')
 ifdef UNSAVED_FILES
@@ -134,6 +138,40 @@ Then, you may want to consider whether you want to restore the autosaves)
 #run.
 endif

+# Check that every compiled file around has a known source file.
+# This should help preventing weird compilation failures caused by leftover
+# compiled files after deleting or moving some source files.
+
+EXISTINGVO:=$(call find, '*.vo')
+KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v'))
+ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO))
+
+EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa')
+KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \
+ $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp))
+KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \
+ $(MLIFILES:.mli=.cmi) \
+ $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma
+ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS))
+
+ifeq (,$(findstring clean,$(MAKECMDGOALS))) # Skip this for 'make clean' and alii
+ifndef ACCEPT_ALIEN_VO
+ifdef ALIENVO
+$(error Leftover compiled Coq files without known sources: $(ALIENVO); \
+remove them first, for instance via 'make voclean' or 'make alienclean' \
+(or skip this check via 'make ACCEPT_ALIEN_VO=1'))
+endif
+endif
+
+ifndef ACCEPT_ALIEN_OBJ
+ifdef ALIENOBJS
+$(error Leftover compiled OCaml files without known sources: $(ALIENOBJS); \
+remove them first, for instance via 'make clean' or 'make alienclean' \
+(or skip this check via 'make ACCEPT_ALIEN_OBJ=1'))
+endif
+endif
+endif
+
 # Apart from clean and tags, everything will be done in a sub-call to make
 # on Makefile.build. This way, we avoid doing here the -include of .d :
 # since they trigger some compilations, we do not want them for a mere clean.
@@ -163,7 +201,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ;
 # Cleaning
 ###########################################################################

-.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean devdocclean
+.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean alienclean

 clean: objclean cruftclean depclean docclean devdocclean

@@ -185,6 +223,7 @@ indepclean:
 	rm -f test-suite/check.log
 	rm -f glob.dump
 	rm -f config/revision.ml revision
+	rm -f plugins/micromega/.micromega.ml.generated
 	$(MAKE) -C test-suite clean

 docclean:
@@ -197,22 +236,19 @@ docclean:
 	  doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \
 	  doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex
 	rm -f doc/*/*.ps doc/*/*.pdf doc/*/*.eps doc/*/*.pdf_t doc/*/*.eps_t
-	rm -f doc/faq/axioms.png
-	rm -rf doc/refman/html doc/stdlib/html doc/faq/html doc/tutorial/tutorial.v.html
-	rm -f doc/refman/euclid.ml doc/refman/euclid.mli
-	rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli
+	rm -rf doc/stdlib/html doc/tutorial/tutorial.v.html
 	rm -f doc/common/version.tex
-	rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/Reference-Manual.html
 	rm -f doc/coq.tex
+	rm -rf doc/sphinx/_build

 archclean: clean-ide optclean voclean
 	rm -rf _build
 	rm -f $(ALLSTDLIB).*

 optclean:
-	rm -f $(COQTOPEXE) $(COQMKTOP) $(CHICKEN)
+	rm -f $(COQTOPEXE) $(CHICKEN)
 	rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT)
-	find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
+	find . -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f

 clean-ide:
 	rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDE)
@@ -225,26 +261,37 @@ ml4clean:
 	rm -f $(GENML4FILES)

 depclean:
-	find . $(FIND_VCS_CLAUSE) '(' -name '*.d' ')' -print | xargs rm -f
+	find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -print | xargs rm -f

 cacheclean:
 	find theories plugins test-suite -name '.*.aux' -delete

 cleanconfig:
-	rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-v7 config/Info-*.plist
+	rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist

-distclean: clean cleanconfig cacheclean
+distclean: clean cleanconfig cacheclean timingclean

 voclean:
 	find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -delete
 	find theories plugins test-suite -name .coq-native -empty -delete

+timingclean:
+	find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' -o -name "*.v.after-timing" -o -name "*.v.timing.diff" -o -name "time-of-build.log" -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -delete
+
 devdocclean:
 	find . -name '*.dep.ps' -o -name '*.dot' | xargs rm -f
 	rm -f $(OCAMLDOCDIR)/*.log $(OCAMLDOCDIR)/*.aux $(OCAMLDOCDIR)/*.toc
 	rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex
 	rm -f $(OCAMLDOCDIR)/html/*.html

+alienclean:
+	rm -f $(ALIENOBJS) $(ALIENVO)
+
+###########################################################################
+# Continuous Intregration Tests
+###########################################################################
+include Makefile.ci
+
 ###########################################################################
 # Emacs tags
 ###########################################################################
@@ -288,4 +335,3 @@ printenv:
 	@env | wc -L
 	@echo -n "Total (win32 limit is 32k) : "
 	@env | wc -m
-
--- a/Makefile.build
+++ b/Makefile.build
--- a/Makefile.checker
+++ b/Makefile.checker
-#######################################################################
-#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
-# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
-#   \VV/  #############################################################
-#    //   #      This file is distributed under the terms of the      #
-#         #       GNU Lesser General Public License Version 2.1       #
-#######################################################################
+##########################################################################
+##         #   The Coq Proof Assistant / The Coq Development Team       ##
+##  v      #   INRIA, CNRS and contributors - Copyright 1999-2018       ##
+## <O___,, #       (see CREDITS file for the list of authors)           ##
+##   \VV/  ###############################################################
+##    //   #    This file is distributed under the terms of the         ##
+##         #     GNU Lesser General Public License Version 2.1          ##
+##         #     (see LICENSE file for the text of the license)         ##
+##########################################################################

 ## Makefile rules for building Coqchk

@@ -20,16 +22,22 @@ CHICKEN:=bin/coqchk$(EXE)

 # The sources

-CHKLIBS:= -I config -I lib -I checker
+CHKLIBS:= -I config -I clib -I lib -I checker

 ## NB: currently, both $(OPTFLAGS) and $(BYTEFLAGS) contain -thread

 # The rules

+CHECKMLDFILE := checker/.mlfiles
+CHECKMLLIBFILE := checker/.mllibfiles
+
+CHECKERDEPS := $(addsuffix .d, $(CHECKMLDFILE) $(CHECKMLLIBFILE))
+-include $(CHECKERDEPS)
+
 ifeq ($(BEST),opt)
-$(CHICKEN): checker/check.cmxa checker/main.ml
+$(CHICKEN): checker/check.cmxa checker/main.mli checker/main.ml
 	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLOPT) $(SYSCMXA) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
+	$(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^
 	$(STRIP) $@
 	$(CODESIGN) $@
 else
@@ -37,9 +45,9 @@ $(CHICKEN): $(CHICKENBYTE)
 	cp $< $@
 endif

-$(CHICKENBYTE): checker/check.cma checker/main.ml
+$(CHICKENBYTE): checker/check.cma checker/main.mli checker/main.ml
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(SYSCMA) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^
+	$(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^

 checker/check.cma: checker/check.mllib | md5chk
 	$(SHOW)'OCAMLC -a -o $@'
@@ -49,17 +57,13 @@ checker/check.cmxa: checker/check.mllib | md5chk
 	$(SHOW)'OCAMLOPT -a -o $@'
 	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^)

-checker/%.ml.d: checker/%.ml
-	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) "$<" $(TOTARGET)
-
-checker/%.mli.d: checker/%.mli
-	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) "$<" $(TOTARGET)
+$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES))
+	$(SHOW)'OCAMLDEP  checker/MLFILES checker/MLIFILES'
+	$(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(filter checker/%, $(MLFILES) $(MLIFILES)) $(TOTARGET)

-checker/%.mllib.d: checker/%.mllib | $(OCAMLLIBDEP)
-	$(SHOW)'OCAMLLIBDEP  $<'
-	$(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) "$<" $(TOTARGET)
+$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) | $(OCAMLLIBDEP)
+	$(SHOW)'OCAMLLIBDEP  checker/MLLIBFILES checker/MLPACKFILES'
+	$(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES)) $(TOTARGET)

 checker/%.cmi: checker/%.mli
 	$(SHOW)'OCAMLC    $<'
@@ -71,12 +75,12 @@ checker/%.cmo: checker/%.ml

 checker/%.cmx: checker/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(HACKMLI) -c $<
+	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -c $<

 md5chk:
 	$(SHOW)'MD5SUM cic.mli'
-	$(HIDE)if grep -q `$(MD5SUM) checker/cic.mli` checker/values.ml; \
-	       then true; else echo "Error: outdated checker/values.ml"; false; fi
+	$(HIDE)if grep -q "^MD5 $$($(OCAML) tools/md5sum.ml checker/cic.mli)$$" checker/values.ml; \
+	       then true; else echo "Error: outdated checker/values.ml" >&2; false; fi

 .PHONY: md5chk


--- a/Makefile.ci
+++ b/Makefile.ci
+##########################################################################
+##         #   The Coq Proof Assistant / The Coq Development Team       ##
+##  v      #   INRIA, CNRS and contributors - Copyright 1999-2018       ##
+## <O___,, #       (see CREDITS file for the list of authors)           ##
+##   \VV/  ###############################################################
+##    //   #    This file is distributed under the terms of the         ##
+##         #     GNU Lesser General Public License Version 2.1          ##
+##         #     (see LICENSE file for the text of the license)         ##
+##########################################################################
+
+CI_TARGETS=ci-bedrock2 \
+    ci-bignums \
+    ci-color \
+    ci-compcert \
+    ci-coq-dpdgraph \
+    ci-coquelicot \
+    ci-corn \
+    ci-cpdt \
+    ci-elpi \
+    ci-ext-lib \
+    ci-equations \
+    ci-fcsl-pcm \
+    ci-fiat-crypto \
+    ci-fiat-crypto-legacy \
+    ci-fiat-parsers \
+    ci-flocq \
+    ci-formal-topology \
+    ci-geocoq \
+    ci-hott \
+    ci-iris-lambda-rust \
+    ci-ltac2 \
+    ci-math-classes \
+    ci-math-comp \
+    ci-mtac2 \
+    ci-quickchick \
+    ci-sf \
+    ci-simple-io \
+    ci-tlc \
+    ci-unimath \
+    ci-vst
+
+.PHONY: ci-all $(CI_TARGETS)
+
+ci-help:
+	echo '*** Coq CI system, please specify a target to build.'
+	false
+
+ci-all: $(CI_TARGETS)
+
+ci-color: ci-bignums
+
+ci-math-classes: ci-bignums
+
+ci-corn: ci-math-classes
+
+ci-quickchick: ci-ext-lib ci-simple-io
+
+ci-formal-topology: ci-corn
+
+# Generic rule, we use make to ease travis integration with mixed rules
+$(CI_TARGETS): ci-%:
+	+./dev/ci/ci-wrapper.sh $*
+
+# For emacs:
+# Local Variables:
+# mode: makefile
+# End: