diff --git a/.gitignore b/.gitignore
index 3321a46bec4d8b16258bf202a30ce4a40a76f1cb..0240dcae454d0ebd6f911ff02f7be999e1b2110f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -17,3 +17,4 @@
 auto
 *.fmt
 coq/*/Makefile.coq
+*~
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index a2721c107464bafc70d7ad9b750c5c9f7e1a49b4..a9d10061a891e31a1370c19988734329f1603362 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,89 +1,21 @@
-image: coq:8.5
+image: ralfjung/opam-ci:latest
 
-stages:
-  - depsquick
-  - depsfull
-  - quickbuild
-  - quickcheck
-  - fullbuild
-
-iris-quick:
-  stage: depsquick
-  tags:
-  - coq
-  script: >
-    (git --version || (apt-get update && apt-get install -y git));
-    git submodule update --init --recursive;
-    cd coq/iris;
-    cat _CoqProject | grep -v '^test' > _CoqProject_filtered;
-    mv _CoqProject_filtered _CoqProject;
-    make -j8 quick;
-    git checkout _CoqProject
-  only:
-  - master
-
-iris-full:
-  stage: depsfull
-  tags:
-  - coq
-  script: >
-    (git --version || (apt-get update && apt-get install -y git));
-    git submodule update --init --recursive;
-    cd coq/iris;
-    cat _CoqProject | grep -v '^test' > _CoqProject_filtered;
-    mv _CoqProject_filtered _CoqProject;
-    make -j8;
-    git checkout _CoqProject
-  only:
-  - master
-
-# vio:
-#   stage: quickbuild
-#   tags:
-#   - coq
-#   script: >
-#     cd coq/ra/;
-#     coqc -v;
-#     time make -j8 TIMED=y quick 2>&1 | tee build-log-vio.txt;
-#     cat build-log-vio.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio.txt
-#   only:
-#   - master
-#   cache:
-#     paths:
-#     - coq/ra/*.vio
-#   artifacts:
-#     paths:
-#     - coq/ra/build-time-vio.txt
-
-# vio2vo:
-#   stage: quickcheck
-#   tags:
-#   - coq
-#   script: >
-#     cd coq/ra/;
-#     coqc -v;
-#     time make -j8 TIMED=y vio2vo J=8 2>&1 | tee build-log-vio2vo.txt;
-#     cat build-log-vio2vo.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio2vo.txt
-#   only:
-#   - master
-#   allow_failure: true
-#   artifacts:
-#     paths:
-#     - coq/ra/build-time-vio2vo.txt
-
-full:
-  stage: fullbuild
-  tags:
-  - coq
-  script: >
-    cd coq/ra/;
-    coqc -v;
-    make clean;
-    time make -j8 TIMED=y 2>&1 | tee build-log-full.txt;
-    fgrep Axiom build-log-full.txt && exit 1;
-    cat build-log-full.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-full.txt;
+gps-coq8.5.3:
+  script:
+  # prepare
+  - cd coq
+  - . build/opam-ci.sh 'coq 8.5.3' 'coq-mathcomp-ssreflect 1.6'
+  # build (the script above switched us to the right directory)
+  - 'time make -j8 TIMED=y 2>&1 | tee build-log-full.txt'
+  - 'if fgrep Axiom build-log-full.txt >/dev/null; then exit 1; fi'
+  - 'cat build-log-full.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-full.txt'
+  cache:
+    key: "coq8.5.3"
+    paths:
+    - coq/opamroot/
   only:
   - master
+  - opam-ci
   artifacts:
     paths:
     - coq/ra/build-time-full.txt
diff --git a/.gitmodules b/.gitmodules
deleted file mode 100644
index 0f782ad0369c60078bec32b6664f097f3d8f9eaa..0000000000000000000000000000000000000000
--- a/.gitmodules
+++ /dev/null
@@ -1,3 +0,0 @@
-[submodule "coq/iris"]
-	path = coq/iris
-	url = https://gitlab.mpi-sws.org/FP/iris-coq.git
diff --git a/coq/build/opam-ci.sh b/coq/build/opam-ci.sh
new file mode 100755
index 0000000000000000000000000000000000000000..d29ed6e532ab5526d6b205037ca772967ba5e2a9
--- /dev/null
+++ b/coq/build/opam-ci.sh
@@ -0,0 +1,34 @@
+#!/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
+opam install ocamlfind -y # Remove this once the Coq crew fixed their package...
+
+# Install fixed versions of some dependencies
+echo
+for PIN in "${@}"
+do
+    echo "Applying pin: $PIN"
+    opam pin add $PIN -k version -y
+done
+
+# Install build-dependencies
+echo
+cd ra
+make build-dep Y=1
+
+# done
+echo
+coqc -v
diff --git a/coq/build/opam-pins.sh b/coq/build/opam-pins.sh
new file mode 100755
index 0000000000000000000000000000000000000000..aebd23ca2589992274146d8c37ebd2eb7489ac31
--- /dev/null
+++ b/coq/build/opam-pins.sh
@@ -0,0 +1,17 @@
+#!/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
+    echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
+    opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
+    echo
+done
diff --git a/coq/iris b/coq/iris
deleted file mode 160000
index 6e00aa3402b729fb58e5dd0c95d18156ca70c3a2..0000000000000000000000000000000000000000
--- a/coq/iris
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 6e00aa3402b729fb58e5dd0c95d18156ca70c3a2
diff --git a/coq/ra/Makefile b/coq/ra/Makefile
index ff1ccd39b120b9d1ff5e72d079d8484bfbfb551b..f26c5ef72a2cb382d6c77239f5d0c338394dae20 100644
--- a/coq/ra/Makefile
+++ b/coq/ra/Makefile
@@ -1,22 +1,51 @@
-# Makefile originally taken from coq-club
+# Process flags
+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
+endif
+
+# Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
-	+make -f Makefile.coq $@
+	+@make -f Makefile.coq $@
 
 all: Makefile.coq
-	+make -f Makefile.coq all
+	+@make -f Makefile.coq all
 
 clean: Makefile.coq
-	+make -f Makefile.coq clean
+	+@make -f Makefile.coq clean
+	find \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
 	rm -f Makefile.coq
 
+# Create Coq Makefile
 Makefile.coq: _CoqProject Makefile
-	coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq
-
-_CoqProject: ;
-
+	@# we want to pass the correct name to coq_makefile or it will be confused.
+	coq_makefile $(COQ_MAKEFILE_FLAGS) -f _CoqProject -o Makefile.coq
+	mv Makefile.coq Makefile.coq.tmp
+	@# The sed script is for Coq 8.5 only, it fixes 'make verify'.
+	@# The awk script fixes 'make uninstall'.
+	sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' < Makefile.coq.tmp \
+	  | awk '/^uninstall:/{print "uninstall:";print "\tif [ -d \"$$(DSTROOT)\"$$(COQLIBINSTALL)/iris/ ]; then find \"$$(DSTROOT)\"$$(COQLIBINSTALL)/iris/ -name \"*.vo\" -print -delete; fi";getline;next}1' > Makefile.coq
+	rm Makefile.coq.tmp
+
+# Install build-dependencies
+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-gps "$$(pwd)/../..#HEAD" -k git -n -y
+	opam install coq-gps --deps-only $(YFLAG)
+	opam pin remove coq-gps
+
+# some fiels that do *not* need to be forwarded to Makefile.coq
 Makefile: ;
+_CoqProject: ;
 
+# Phony targets (i.e. targets that should be run no matter the timestamps of the involved files)
 phony: ;
-
 .PHONY: all clean phony
diff --git a/coq/ra/_CoqProject b/coq/ra/_CoqProject
index 946ef7b8ebb78ce0e55c8f7e210a97213b323ef2..0c87d9c3b0a7ff7d89f6e5c70e4c3804930e8edd 100644
--- a/coq/ra/_CoqProject
+++ b/coq/ra/_CoqProject
@@ -1,5 +1,4 @@
 -R . ra
--Q ../iris iris
 ./infrastructure.v
 ./types.v
 ./views.v
diff --git a/opam b/opam
new file mode 100644
index 0000000000000000000000000000000000000000..69ed1f364f0f765288e0ed5b2e343a1445d352ce
--- /dev/null
+++ b/opam
@@ -0,0 +1,17 @@
+opam-version: "1.2"
+name: "coq-gps"
+version: "dev"
+maintainer: "Jan-Oliver Kaiser, Hoang-Hai Dang"
+authors: "Jan-Oliver Kaiser, Hoang-Hai Dang"
+# homepage: "?"
+bug-reports: "https://gitlab.mpi-sws.org/FP/sra-gps/issues"
+dev-repo: "https://gitlab.mpi-sws.org/FP/sra-gps.git"
+build: [
+  [make "-j%{jobs}%"]
+]
+install: [make "install"]
+# TODO: probably we want to install things to a different folder, "ra" is rather undescriptive
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/ra" ]
+depends: [
+  "coq-iris"
+]
diff --git a/opam.pins b/opam.pins
new file mode 100644
index 0000000000000000000000000000000000000000..9625cdc6ef2c8f9a32a1505b19da879a0b5d2468
--- /dev/null
+++ b/opam.pins
@@ -0,0 +1 @@
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 6e00aa3402b729fb58e5dd0c95d18156ca70c3a2