Skip to content
Snippets Groups Projects
Commit b1c2c3df authored by Ralf Jung's avatar Ralf Jung
Browse files

remove some unused imports

parent 244530d5
No related branches found
No related tags found
No related merge requests found
Pipeline #36826 passed
...@@ -2,7 +2,6 @@ ...@@ -2,7 +2,6 @@
(** A resource algebra for the specification programs. *) (** A resource algebra for the specification programs. *)
From iris.algebra Require Import auth excl gmap agree list frac. From iris.algebra Require Import auth excl gmap agree list frac.
From iris.bi Require Export fractional. From iris.bi Require Export fractional.
From iris.base_logic Require Import gen_heap.
From iris.base_logic Require Export invariants. From iris.base_logic Require Export invariants.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import lang primitive_laws. From iris.heap_lang Require Import lang primitive_laws.
......
(* ReLoC -- Relational logic for fine-grained concurrency *) (* ReLoC -- Relational logic for fine-grained concurrency *)
(** Rules for updating the specification program. *) (** Rules for updating the specification program. *)
From iris.algebra Require Import auth excl frac agree gmap list. 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.proofmode Require Import tactics.
From iris.heap_lang Require Export lang notation tactics. From iris.heap_lang Require Export lang notation tactics.
From reloc.logic Require Export spec_ra. From reloc.logic Require Export spec_ra.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment