From ed36f0c1b01852fea68a60c1fb30df072ac37918 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 21 Sep 2017 09:09:56 +0200
Subject: [PATCH] make it compatible with Coq 8.7, and test that

---
 .gitlab-ci.yml            | 6 ++++++
 theories/history.v        | 6 +++---
 theories/infrastructure.v | 2 +-
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 580518d1..af344b4c 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 ca5b84f4..3c5c584c 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 bcee7610..0695b7bd 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+.
-- 
GitLab