From f8e2c74ce745f092c4d20e9ef855d7657e25134c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 6 Dec 2016 17:32:47 +0100
Subject: [PATCH] compatibility with coq 8.6

---
 heap_lang/lib/assert.v        | 3 ++-
 heap_lang/lib/barrier/proof.v | 2 ++
 heap_lang/lib/counter.v       | 3 ++-
 heap_lang/lib/par.v           | 3 ++-
 heap_lang/lib/spawn.v         | 2 +-
 heap_lang/lib/spin_lock.v     | 4 +++-
 heap_lang/lib/ticket_lock.v   | 3 +--
 tests/barrier_client.v        | 3 ++-
 tests/counter.v               | 3 ++-
 tests/joining_existentials.v  | 3 ++-
 tests/one_shot.v              | 3 ++-
 tests/tree_sum.v              | 5 +++--
 12 files changed, 24 insertions(+), 13 deletions(-)

diff --git a/heap_lang/lib/assert.v b/heap_lang/lib/assert.v
index 547f96158..4de019169 100644
--- a/heap_lang/lib/assert.v
+++ b/heap_lang/lib/assert.v
@@ -7,7 +7,6 @@ Definition assert : val :=
   λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
 (* just below ;; *)
 Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
-Global Opaque assert.
 
 Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
   WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} ⊢ WP assert: e @ E {{ Φ }}.
@@ -15,3 +14,5 @@ Proof.
   iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
   iApply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
 Qed.
+
+Global Opaque assert.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 2b65b88c7..b67477be2 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -22,6 +22,8 @@ Section proof.
 Context `{!heapG Σ, !barrierG Σ} (N : namespace).
 Implicit Types I : gset gname.
 
+Local Transparent newbarrier signal wait.
+
 Definition ress (P : iProp Σ) (I : gset gname) : iProp Σ :=
   (∃ Ψ : gname → iProp Σ,
     ▷ (P -∗ [∗ set] i ∈ I, Ψ i) ∗ [∗ set] i ∈ I, saved_prop_own i (Ψ i))%I.
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index 941ae644e..4391887a8 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -10,7 +10,6 @@ Definition incr : val :=
     let: "n" := !"l" in
     if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
 Definition read : val := λ: "l", !"l".
-Global Opaque newcounter incr get.
 
 (** Monotone counter *)
 Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
@@ -167,3 +166,5 @@ Section contrib_spec.
     by iApply "HΦ".
   Qed.
 End contrib_spec.
+
+Global Opaque newcounter incr get.
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 52eae597b..6b4b310aa 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -11,7 +11,6 @@ Definition par : val :=
     let: "v1" := join "handle" in
     ("v1", "v2").
 Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
-Global Opaque par.
 
 Section proof.
 Context `{!heapG Σ, !spawnG Σ}.
@@ -45,3 +44,5 @@ Proof.
   iSplitL "H1"; by wp_let.
 Qed.
 End proof.
+
+Global Opaque par.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 17c44630a..d424aa7fa 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -14,7 +14,6 @@ Definition join : val :=
       SOME "x" => "x"
     | NONE => "join" "c"
     end.
-Global Opaque spawn join.
 
 (** The CMRA & functor we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
@@ -79,3 +78,4 @@ Qed.
 End proof.
 
 Typeclasses Opaque join_handle.
+Global Opaque spawn join.
diff --git a/heap_lang/lib/spin_lock.v b/heap_lang/lib/spin_lock.v
index 896caade9..46e8715bc 100644
--- a/heap_lang/lib/spin_lock.v
+++ b/heap_lang/lib/spin_lock.v
@@ -10,7 +10,6 @@ Definition try_acquire : val := λ: "l", CAS "l" #false #true.
 Definition acquire : val :=
   rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
 Definition release : val := λ: "l", "l" <- #false.
-Global Opaque newlock try_acquire acquire release.
 
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
@@ -89,6 +88,9 @@ Section proof.
   Qed.
 End proof.
 
+Typeclasses Opaque is_lock locked.
+Global Opaque newlock try_acquire acquire release.
+
 Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
   {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 194b3da1f..eab626e56 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -25,8 +25,6 @@ Definition acquire : val :=
 Definition release : val := λ: "lk",
   (Fst "lk") <- !(Fst "lk") + #1.
 
-Global Opaque newlock acquire release wait_loop.
-
 (** The CMRAs we need. *)
 Class tlockG Σ :=
   tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))).
@@ -170,6 +168,7 @@ Section proof.
 End proof.
 
 Typeclasses Opaque is_lock issued locked.
+Global Opaque newlock acquire release wait_loop.
 
 Definition ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
   {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 6b60585dc..1800ad32c 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -11,7 +11,6 @@ Definition client : expr :=
   let: "b" := newbarrier #() in
   ("y" <- (λ: "z", "z" + #42) ;; signal "b") |||
     (worker 12 "b" "y" ||| worker 17 "b" "y").
-Global Opaque worker client.
 
 Section client.
   Context `{!heapG Σ, !barrierG Σ, !spawnG Σ} (N : namespace).
@@ -55,6 +54,8 @@ Section client.
 Qed.
 End client.
 
+Global Opaque worker client.
+
 Section ClosedProofs.
 
 Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
diff --git a/tests/counter.v b/tests/counter.v
index 9bc8d14b9..4b852ad6d 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -16,7 +16,6 @@ Definition incr : val :=
     let: "n" := !"l" in
     if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
 Definition read : val := λ: "l", !"l".
-Global Opaque newcounter incr read.
 
 (** The CMRA we need. *)
 Inductive M := Auth : nat → M | Frag : nat → M | Bot.
@@ -137,3 +136,5 @@ Proof.
   iModIntro; rewrite /C; eauto 10 with omega.
 Qed.
 End proof.
+
+Global Opaque newcounter incr read.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 0c3f3cb3f..700017967 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -21,7 +21,6 @@ Proof. apply subG_inG. Qed.
 Definition client eM eW1 eW2 : expr :=
   let: "b" := newbarrier #() in
   (eM ;; signal "b") ||| ((wait "b" ;; eW1) ||| (wait "b" ;; eW2)).
-Global Opaque client.
 
 Section proof.
 Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}.
@@ -98,3 +97,5 @@ Proof.
   - iIntros (_ v) "[_ H]". iDestruct (Q_res_join with "H") as "?". auto.
 Qed.
 End proof.
+
+Global Opaque client.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 04c0354c2..323f8896a 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -18,7 +18,6 @@ Definition one_shot_example : val := λ: <>,
        | SOME "m" => assert: "n" = "m"
        end
     end)).
-Global Opaque one_shot_example.
 
 Definition one_shotR := csumR (exclR unitC) (dec_agreeR Z).
 Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR).
@@ -97,3 +96,5 @@ Proof.
     iApply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
 Qed.
 End proof.
+
+Global Opaque one_shot_example.
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index 8e3b9b9c4..bc216d653 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -33,8 +33,6 @@ Definition sum' : val := λ: "t",
   sum_loop "t" "l";;
   !"l".
 
-Global Opaque sum_loop sum'.
-
 Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) (Φ : val → iProp Σ) :
   heap_ctx ∗ l ↦ #n ∗ is_tree v t
     ∗ (l ↦ #(sum t + n) -∗ is_tree v t -∗ Φ #())
@@ -66,3 +64,6 @@ Proof.
   rewrite Z.add_0_r.
   iIntros "Hl Ht". wp_seq. wp_load. by iApply "HΦ".
 Qed.
+
+Global Opaque sum_loop sum'.
+
-- 
GitLab