diff --git a/Makefile b/Makefile
index 8d615e4b2c9081e20b16fb3931cea5ef951c540c..331cb03f841de9ffc5711e876acd402e4816fb87 100644
--- a/Makefile
+++ b/Makefile
@@ -8,7 +8,7 @@ all: Makefile.coq
 
 clean: Makefile.coq
 	+@make -f Makefile.coq clean
-	find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
+	find theories tests exercises solutions \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
 	rm -f Makefile.coq .lia.cache
 .PHONY: clean
 
diff --git a/opam b/opam
index df51f92091fc6c78bf6c78c3bc8a9d196dfdd485..46fb02f8868561149088a0d6b101ca817b657686 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-06-06.0.d7449e86") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-06-19.0.1c30e9d2") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 09bfa2b4ce1d28587f15841ebfa7cfa344ac5c2a..07ec46d14c9fbefe0ca963312f77d2a6ef669e67 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -2,7 +2,7 @@ From Coq.QArith Require Import Qcanon.
 From iris.base_logic.lib Require Import invariants.
 From iris.proofmode Require Import tactics.
 From iris.bi Require Import fractional.
-From iris.algebra Require Import excl csum frac auth agree.
+From iris.algebra Require Import excl csum frac auth agree numbers.
 From lrust.lang Require Import notation.
 From gpfsl.gps Require Import middleware protocols.
 From gpfsl.logic Require Import view_invariants.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index b1bb413862cb9a8153b9de27d37ce4d6f2f8427a..df30fe502a2f9267d05b0781b2576e098884d2e6 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -1,6 +1,6 @@
 From lrust.lifetime Require Export primitive.
 From lrust.lifetime Require Import faking.
-From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.algebra Require Import csum auth frac gmap agree gset numbers.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 53db3b02cdcda87a685a3f34b854ab657a1718ea..ee6fbc8599ddd2dc4e321dbae362443accb4b38f 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import csum auth excl frac gmap agree gset.
+From iris.algebra Require Import csum auth excl frac gmap agree gset numbers.
 From lrust.lifetime.model Require Import boxes.
 From lrust.lifetime Require Export lifetime_sig.
 From gpfsl.base_logic Require Export lattice_cmra.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 0704936e5dbd789a3d396700031b36692831765b..23f13c27da42cfa91c6f7015fb042fda1aef5491 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -1,5 +1,5 @@
 From lrust.lifetime.model Require Export primitive.
-From iris.algebra Require Import csum auth excl frac gmap agree gset.
+From iris.algebra Require Import csum auth excl frac gmap agree gset numbers.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index debb35eb4ac847fc1941a20c08ef3ed863b058f1..0622b4126e5ebc09bda751d450b334d10ae86df8 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -1,5 +1,5 @@
 From lrust.lifetime Require Import borrow accessors.
-From iris.algebra Require Import csum auth excl frac gmap agree gset.
+From iris.algebra Require Import csum auth excl frac gmap agree gset numbers.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 35a255fb617b8c0e65444207395c07c446a546d8..a098f55a2973fd0c0d82ab7f798b3c6023045b13 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -1,5 +1,5 @@
 From Coq.QArith Require Import Qcanon.
-From iris.algebra Require Import auth excl csum frac agree.
+From iris.algebra Require Import auth excl csum frac agree numbers.
 From lrust.lang Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index b91f07af1757ecbee8702e136fc0f482bf3ad6e1..77586f496d796954b40baab8b93a307cd862e125 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree numbers.
 From lrust.lang Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 4ea4c7c55c94d2fb35a1589a8cd9357cf5327637..4a42835ef1e67a1dfaa213d80333c12a1f490b0a 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -1,5 +1,5 @@
 From Coq.QArith Require Import Qcanon.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import lifetime na_borrow.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 45cb8549ce6f23495561a07ee6d7f0df4677cef8..1341fca878b801c7f8d30f28dbd68006c69d465c 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 8863fcbc9ede513de3c4d5b2cb82ffa47e075cab..bc776ababd5da3b854a8fc567fafd8b3f23be5c4 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -1,5 +1,5 @@
 From Coq.QArith Require Import Qcanon.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree numbers.
 From iris.bi Require Import fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 5efbe5568a6a6e7ccee515bde0e39250cb092a8b..248132e699e00fd4560d1727dfd2cdfbfbfc1e2b 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -1,7 +1,7 @@
 From Coq.QArith Require Import Qcanon.
 From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth excl csum frac agree.
+From iris.algebra Require Import auth excl csum frac agree numbers.
 From gpfsl.gps Require Import middleware protocols.
 From lrust.lifetime Require Import at_borrow.
 From lrust.typing Require Import typing.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index aae742a91e79885aaa3382e8878381232002fce1..ecd96a9751d960039344ea2fc2e1fce51d19224a 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -1,7 +1,7 @@
 From Coq.QArith Require Import Qcanon.
 From iris.bi Require Import fractional.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import auth csum frac agree.
+From iris.algebra Require Import auth csum frac agree numbers.
 From gpfsl.gps Require Import middleware protocols.
 From lrust.logic Require Import gps.
 From lrust.lifetime Require Import at_borrow.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index a1c70ad919878bb653b6705c25787c7846c8e4c6..9abc418ecd44b5ac99850728454d2bfa88ecdc3d 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import list.
+From iris.algebra Require Import list numbers.
 From lrust.typing Require Import lft_contexts.
 From lrust.typing Require Export type.
 Set Default Proof Using "Type".
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index ac4177678019c775375159806cad513006c954ec..4463e0d1ab5cc31b97ae8a83577af3a82debddcc 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -1,4 +1,5 @@
 From Coq Require Import Qcanon.
+From iris.algebra Require Import numbers.
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 1ed100d0b692a8f3458027a7aa54d28104c0a04a..7515f0b35361b6d3c0c381f9b0e516ad3c8d41d0 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -1,3 +1,4 @@
+From iris.algebra Require Import numbers.
 From gpfsl.lang Require Export notation.
 From gpfsl.base_logic Require Export na.
 From gpfsl.logic Require Export na_invariants.