diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 580518d1aec9451f6736408db6ba07f5216d0ade..af344b4cfade73ec7039731220d9629c8abe080c 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -23,6 +23,12 @@ variables:
   - master
   - /^ci/
 
+iris-coq8.7:
+  <<: *template
+  variables:
+    COQ_VERSION: "8.7.dev"
+    SSR_VERSION: "dev"
+
 igps-coq8.6.1:
   <<: *template
   variables:
diff --git a/theories/history.v b/theories/history.v
index ca5b84f48e1c2a9582d6e60adc631e57626419b9..3c5c584c5589dfcd2f0bd99b311cd41dad4edee6 100644
--- a/theories/history.v
+++ b/theories/history.v
@@ -143,7 +143,7 @@ Section History.
         destruct (Pos.lt_total (mtime m') (mtime m)) as [|[Eq|Gt]] => //;
           exfalso.
           * destruct (memory_ok _ _ _ Inm' Inm) as [Eqm|[|]] => //.
-            by rewrite Eqm Valm in EqD.
+            by rewrite /= Eqm Valm in EqD.
           * specialize (ValGE _ Inm' EqLoc Gt). rewrite EqD in ValGE.
             by inversion ValGE.
     - apply (MT_impl TA).
@@ -153,7 +153,7 @@ Section History.
         destruct (Pos.lt_total (mtime m') (mtime m)) as [|[Eq|Gt]] => //;
           exfalso.
           * destruct (memory_ok _ _ _ Inm' Inm) as [Eqm|[|]] => //.
-            by rewrite Eqm Valm in EqD.
+            by rewrite /= Eqm Valm in EqD.
           * specialize (ValGE _ Inm' EqLoc Gt). rewrite EqD in ValGE.
             by inversion ValGE.
     - assert (In:= MT_msg_In TA).
@@ -161,4 +161,4 @@ Section History.
       rewrite -> 2!elem_of_filter in In. by destruct In as [_ []].
   Qed.
 
-End History.
\ No newline at end of file
+End History.
diff --git a/theories/infrastructure.v b/theories/infrastructure.v
index bcee76108bcf6d744b8fccc4f61de2d760de73a9..0695b7bd053076bf12c5c8d9751a721dd262bea1 100644
--- a/theories/infrastructure.v
+++ b/theories/infrastructure.v
@@ -322,7 +322,7 @@ Section Filter_Help.
   Global Instance lfold_Unfold `{fhl1 : list lType} M2 m Q:
     SetUnfold (m ∈ M2) (Q) ->
     SetUnfold (m ∈ lfold M2 (fhl1))
-              (fold_right (λ s : lType, let (P, _) := s in and (P m)) (Q) (fhl1)).
+              (fold_right (λ s : lType, and (projT1 s m)) (Q) (fhl1)).
   Proof.
     intros SU. constructor. revert m SU.
     induction fhl1 => /=; first abstract set_solver+.