From c390d51246998fdcda2730977b5dd891ddeef1d3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 5 Aug 2016 17:10:10 +0200
Subject: [PATCH] =?UTF-8?q?Clean=20up=20Imports=20so=20that=20the=20=3D{E}?=
 =?UTF-8?q?=3D=E2=98=85=20notation=20is=20displayed=20properly.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 heap_lang/lib/assert.v        | 2 ++
 heap_lang/lib/barrier/proof.v | 4 +++-
 heap_lang/lib/counter.v       | 1 +
 heap_lang/lib/lock.v          | 1 +
 heap_lang/lib/spawn.v         | 1 +
 heap_lang/lib/ticket_lock.v   | 6 ++++--
 program_logic/auth.v          | 6 +++---
 program_logic/boxes.v         | 4 ++--
 program_logic/sts.v           | 4 ++--
 tests/barrier_client.v        | 3 ++-
 tests/heap_lang.v             | 4 +++-
 tests/joining_existentials.v  | 5 +++--
 tests/list_reverse.v          | 3 ++-
 tests/one_shot.v              | 5 +++--
 tests/tree_sum.v              | 2 ++
 15 files changed, 34 insertions(+), 17 deletions(-)

diff --git a/heap_lang/lib/assert.v b/heap_lang/lib/assert.v
index 4e62f488b..bae4e2c03 100644
--- a/heap_lang/lib/assert.v
+++ b/heap_lang/lib/assert.v
@@ -1,3 +1,5 @@
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 5b43b5fdd..55c8a2fc4 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -1,8 +1,10 @@
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang.lib.barrier Require Export barrier.
 From iris.prelude Require Import functions.
 From iris.algebra Require Import upred_big_op.
 From iris.program_logic Require Import saved_prop sts.
 From iris.heap_lang Require Import proofmode.
-From iris.heap_lang.lib.barrier Require Export barrier.
 From iris.heap_lang.lib.barrier Require Import protocol.
 
 (** The CMRAs we need. *)
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index e1677077e..9678f3f5d 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -1,3 +1,4 @@
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import invariants tactics.
 From iris.program_logic Require Import auth.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 080bb3d6c..6f3b9b5bd 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -1,3 +1,4 @@
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import invariants tactics.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index af61860e2..dfdd1bcef 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -1,3 +1,4 @@
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import invariants tactics.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 190948468..35f0f53db 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -1,5 +1,7 @@
-From iris.program_logic Require Export global_functor auth.
-From iris.proofmode Require Import invariants ghost_ownership.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.program_logic Require Import auth.
+From iris.proofmode Require Import invariants.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import gset.
 Import uPred.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index cd77b3052..996e74578 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -1,7 +1,7 @@
-From iris.algebra Require Export auth upred_tactics.
+From iris.program_logic Require Export pviewshifts.
+From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
-From iris.program_logic Require Export invariants ghost_ownership.
-From iris.proofmode Require Import invariants ghost_ownership.
+From iris.proofmode Require Import invariants.
 Import uPred.
 
 (* The CMRA we need. *)
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 59308593d..97a46c231 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Import gmap agree upred_big_op.
-From iris.program_logic Require Import auth saved_prop.
+From iris.program_logic Require Export pviewshifts.
+From iris.algebra Require Import auth gmap agree upred_big_op.
 From iris.proofmode Require Import tactics invariants.
 Import uPred.
 
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 671ee6aa9..e331e34c9 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Export sts upred_tactics.
-From iris.program_logic Require Export invariants.
+From iris.program_logic Require Export pviewshifts.
+From iris.algebra Require Export sts.
 From iris.proofmode Require Import invariants.
 Import uPred.
 
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 111c5aea5..42fe6db30 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -1,8 +1,9 @@
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
 From iris.heap_lang.lib.barrier Require Import proof.
 From iris.heap_lang Require Import par.
 From iris.program_logic Require Import auth sts saved_prop hoare ownership.
 From iris.heap_lang Require Import proofmode.
-Import uPred.
 
 Definition worker (n : Z) : val :=
   λ: "b" "y", wait "b" ;; !"y" #n.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 932aac1d3..c3665bfbc 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -1,5 +1,7 @@
 (** This file is essentially a bunch of testcases. *)
-From iris.program_logic Require Import ownership hoare auth.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.program_logic Require Import ownership hoare.
 From iris.heap_lang Require Import proofmode notation.
 
 Section LangTests.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index e5d2f1f4e..2ddf7d55c 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -1,5 +1,6 @@
+From iris.program_logic Require Export weakestpre hoare.
+From iris.heap_lang Require Export lang.
 From iris.algebra Require Import excl agree csum.
-From iris.program_logic Require Import hoare.
 From iris.heap_lang.lib.barrier Require Import proof specification.
 From iris.heap_lang Require Import notation par proofmode.
 From iris.proofmode Require Import invariants.
@@ -54,7 +55,7 @@ Lemma Q_res_join γ : barrier_res γ Ψ1 ★ barrier_res γ Ψ2 ⊢ ▷ barrier_
 Proof.
   iIntros "[Hγ Hγ']";
   iDestruct "Hγ" as (x) "[#Hγ Hx]"; iDestruct "Hγ'" as (x') "[#Hγ' Hx']".
-  iAssert (▷ (x ≡ x'))%I as "Hxx" .
+  iAssert (▷ (x ≡ x'))%I as "Hxx".
   { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
     rewrite own_valid csum_validI /= agree_validI agree_equivI uPred.later_equivI /=.
     rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index dafe2070b..4ab90f4c5 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -1,6 +1,7 @@
 (** Correctness of in-place list reversal *)
+From iris.program_logic Require Export weakestpre hoare.
+From iris.heap_lang Require Export lang.
 From iris.proofmode Require Export tactics.
-From iris.program_logic Require Export hoare.
 From iris.heap_lang Require Import proofmode notation.
 
 Section list_reverse.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index e644474e6..e09c317b6 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -1,7 +1,8 @@
+From iris.program_logic Require Export weakestpre hoare.
+From iris.heap_lang Require Export lang.
 From iris.algebra Require Import excl dec_agree csum.
-From iris.program_logic Require Import hoare.
 From iris.heap_lang Require Import assert proofmode notation.
-From iris.proofmode Require Import invariants ghost_ownership.
+From iris.proofmode Require Import invariants.
 
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index d188e64b6..18a8a4d89 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -1,3 +1,5 @@
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode notation.
 
-- 
GitLab