make it compatible with Coq 8.7, and test that

.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:

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.

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+.