diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
new file mode 100644
index 0000000000000000000000000000000000000000..9f09343fb08de36f86891a3b9e756a8ec3a81dad
--- /dev/null
+++ b/.gitlab-ci.yml
@@ -0,0 +1,21 @@
+image: ralfjung/opam-ci:latest
+
+stdpp-coq8.6:
+  tags:
+  - coq
+  script:
+  # prepare
+  - . build/opam-ci.sh coq 8.6
+  # build
+  - 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
+  - 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
+  - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
+  - 'make validate'
+  cache:
+    key: "coq8.6"
+    paths:
+    - opamroot/
+  only:
+  - master
+  - ci
+  - timing
diff --git a/Makefile b/Makefile
index db003e171542c0f9a8b32562fb44b2226a42aee1..877492275c72e88614c432f7b316b85b513137dc 100644
--- a/Makefile
+++ b/Makefile
@@ -3,13 +3,8 @@ ifeq ($(Y), 1)
 	YFLAG=-y
 endif
 
-# Determine Coq version
-COQ_VERSION=$(shell coqc --version | egrep -o 'version 8.[0-9]' | egrep -o '8.[0-9]')
-COQ_MAKEFILE_FLAGS ?=
-
-ifeq ($(COQ_VERSION), 8.6)
-	COQ_MAKEFILE_FLAGS += -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-endif
+# Configure Coq warnings
+COQ_MAKEFILE_FLAGS ?= -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
 
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
@@ -32,9 +27,9 @@ Makefile.coq: _CoqProject Makefile awk.Makefile
 build-dep:
 	build/opam-pins.sh < opam.pins
 	opam upgrade $(YFLAG) # it is not nice that we upgrade *all* packages here, but I found no nice way to upgrade only those that we pinned
-	opam pin add coq-prelude "$$(pwd)#HEAD" -k git -n -y
-	opam install coq-prelude --deps-only $(YFLAG)
-	opam pin remove coq-prelude
+	opam pin add coq-stdpp "$$(pwd)#HEAD" -k git -n -y
+	opam install coq-stdpp --deps-only $(YFLAG)
+	opam pin remove coq-stdpp
 
 # Some files that do *not* need to be forwarded to Makefile.coq
 Makefile: ;
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
new file mode 100755
index 0000000000000000000000000000000000000000..c4189bab6cf3199a00526ea958918c909cfd23d5
--- /dev/null
+++ b/build/opam-ci.sh
@@ -0,0 +1,38 @@
+#!/bin/bash
+set -e
+# This script installs the build dependencies for CI builds.
+
+# Prepare OPAM configuration
+export OPAMROOT="$(pwd)/opamroot"
+export OPAMJOBS=16
+export OPAM_EDITOR="$(which false)"
+
+# Make sure we got a good OPAM
+test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
+eval `opam conf env`
+test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 5
+test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
+test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.inria.fr/opam/released -p 10
+opam update
+
+# Install fixed versions of some dependencies
+echo
+while (( "$#" )); do # while there are arguments left
+    PACKAGE="$1" ; shift
+    VERSION="$1" ; shift
+    # Check if the pin is already set
+    if opam pin list | fgrep "$PACKAGE.$VERSION " > /dev/null; then
+        echo "[opam-ci] $PACKAGE already pinned to $VERSION"
+    else
+        echo "[opam-ci] Pinning $PACKAGE to $VERSION"
+        opam pin add "$PACKAGE" "$VERSION" -k version -y
+    fi
+done
+
+# Install build-dependencies
+echo
+make build-dep Y=1
+
+# done
+echo
+coqc -v
diff --git a/build/opam-pins.sh b/build/opam-pins.sh
new file mode 100755
index 0000000000000000000000000000000000000000..669cd99b833df5259808f3b8f3fae1f96f466271
--- /dev/null
+++ b/build/opam-pins.sh
@@ -0,0 +1,21 @@
+#!/bin/bash
+set -e
+## Process an opam.pins file from stdin: Add all the given pins, but don't install anything.
+## Usage:
+##   ./opam-pins.sh < opam.pins
+
+# Process stdin
+while read PACKAGE URL HASH; do
+    if echo "$URL" | egrep '^https://gitlab\.mpi-sws\.org' > /dev/null; then
+        echo "[opam-pins] Recursing into $URL"
+        # an MPI URL -- try doing recursive pin processing
+        curl -f "$URL/raw/$HASH" 2> /dev/null | "$0"
+    fi
+    if opam pin list | fgrep "$PACKAGE.dev.$HASH " > /dev/null; then
+        echo "[opam-pins] $PACKAGE already at commit $HASH"
+    else
+        echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
+        opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
+    fi
+    echo
+done
diff --git a/opam b/opam
new file mode 100644
index 0000000000000000000000000000000000000000..6cf1701d743143f9073b4f9d21348828922c5155
--- /dev/null
+++ b/opam
@@ -0,0 +1,16 @@
+opam-version: "1.2"
+name: "coq-stdpp"
+version: "dev"
+maintainer: "Robbert Krebbers"
+authors: "Robbert Krebbers"
+bug-reports: "https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/issues"
+license: "BSD"
+dev-repo: "https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git"
+build: [
+  [make "-j%{jobs}%"]
+]
+install: [make "install"]
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/coq-stdpp'" ]
+depends: [
+  "coq" { ((>= "8.6" & < "8.7~") | (= "dev"))}
+]
diff --git a/opam.pins b/opam.pins
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391