From b1c2c3df8a3e74861903ed8c59a702962012df1f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 27 Oct 2020 16:17:05 +0100
Subject: [PATCH] remove some unused imports

---
 theories/logic/spec_ra.v    | 1 -
 theories/logic/spec_rules.v | 1 -
 2 files changed, 2 deletions(-)

diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 54c7ace..6636e38 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -2,7 +2,6 @@
 (** A resource algebra for the specification programs. *)
 From iris.algebra Require Import auth excl gmap agree list frac.
 From iris.bi Require Export fractional.
-From iris.base_logic Require Import gen_heap.
 From iris.base_logic Require Export invariants.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang primitive_laws.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 2d79d34..cf519ed 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -1,7 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Rules for updating the specification program. *)
 From iris.algebra Require Import auth excl frac agree gmap list.
-From iris.base_logic.lib Require Import gen_heap.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Export lang notation tactics.
 From reloc.logic Require Export spec_ra.
-- 
GitLab