From 9a81a9a9ef0a9e97bf2f757befa0d4e0a0ac02aa Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Feb 2020 17:53:56 +0100
Subject: [PATCH] Clean up exports in `heap_lang`.

- Export `total_weakestpre` in `lifting` already, like we do for `weakestpre`.
- Do not export modules that are already exported by exported modules.
---
 theories/heap_lang/array.v     | 1 -
 theories/heap_lang/lifting.v   | 2 +-
 theories/heap_lang/proofmode.v | 3 +--
 3 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index e3769b701..c5edacc8e 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -1,7 +1,6 @@
 From stdpp Require Import fin_maps.
 From iris.bi Require Import lib.fractional.
 From iris.proofmode Require Import tactics.
-From iris.program_logic Require Export total_weakestpre weakestpre.
 From iris.heap_lang Require Export lifting.
 From iris.heap_lang Require Import tactics notation.
 Set Default Proof Using "Type".
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 4660d5604..9f403fd1a 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth gmap.
 From iris.base_logic Require Export gen_heap.
 From iris.base_logic.lib Require Export proph_map.
-From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics notation.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 2851575e3..98ea0e675 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -1,8 +1,7 @@
 From iris.proofmode Require Import coq_tactics reduction.
 From iris.proofmode Require Export tactics.
-From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.program_logic Require Import atomic.
-From iris.heap_lang Require Export tactics lifting array.
+From iris.heap_lang Require Export tactics array.
 From iris.heap_lang Require Import notation.
 Set Default Proof Using "Type".
 Import uPred.
-- 
GitLab