diff --git a/opam b/opam
index 84f0313fbd3631c85da14a46ed4da0a41df95414..d68224567cfdefc083f6f61cad41204832a1f479 100644
--- a/opam
+++ b/opam
@@ -10,6 +10,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
-  "coq" { >= "8.7.0" & < "8.8~" }
+  "coq" { >= "8.7.dev" & < "8.8~" }
   "coq-stdpp" { (= "dev.2017-11-12.2") | (= "dev") }
 ]
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 094577409a44b8e0762494449ba3a0ccb6b279fc..3551b7dfa4940d39bc465681d5bef6b11d36c9ec 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -324,14 +324,13 @@ Definition unseal_eqs :=
   uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq,
   uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
   uPred_cmra_valid_eq, uPred_bupd_eq).
-Ltac unseal := rewrite
-  /bi_emp /= /uPred_emp /bi_pure /bi_and /bi_or /bi_impl
-  /bi_forall /bi_exist /bi_internal_eq /bi_sep /bi_wand /bi_plainly
-  /bi_persistently /bi_later /=
-  /sbi_emp /sbi_pure /sbi_and /sbi_or /sbi_impl
-  /sbi_forall /sbi_exist /sbi_internal_eq /sbi_sep /sbi_wand /sbi_plainly
-  /sbi_persistently /=
-  !unseal_eqs /=.
+Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
+  unfold bi_emp; simpl;
+  unfold uPred_emp, bi_pure, bi_and, bi_or, bi_impl, bi_forall, bi_exist,
+  bi_internal_eq, bi_sep, bi_wand, bi_plainly, bi_persistently, bi_later; simpl;
+  unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
+  sbi_internal_eq, sbi_sep, sbi_wand, sbi_plainly, sbi_persistently; simpl;
+  rewrite !unseal_eqs /=.
 End uPred_unseal.
 Import uPred_unseal.
 
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index ed0851fd9a2981fbfdbf792a3594492db7d495d4..44c05c3f19b4168ad28ce0144840b657e90ae58a 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Export ofe.
+Set Primitive Projections.
 
 Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
 Reserved Notation "'emp'".