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

remove unnecessary import

parent 876c5f03
Branches
No related tags found
No related merge requests found
Pipeline #74188 passed
...@@ -6,7 +6,6 @@ zero by two, the result is four. ...@@ -6,7 +6,6 @@ zero by two, the result is four.
From iris.algebra Require Import excl_auth frac_auth numbers. From iris.algebra Require Import excl_auth frac_auth numbers.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import lib.par proofmode notation. From iris.heap_lang Require Import lib.par proofmode notation.
From exercises Require Import ex_03_spinlock.
(** The program as a heap-lang expression. We use the heap-lang [par] module for (** The program as a heap-lang expression. We use the heap-lang [par] module for
parallel composition. *) parallel composition. *)
......
...@@ -6,7 +6,6 @@ zero by two, the result is four. ...@@ -6,7 +6,6 @@ zero by two, the result is four.
From iris.algebra Require Import excl_auth frac_auth numbers. From iris.algebra Require Import excl_auth frac_auth numbers.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import lib.par proofmode notation. From iris.heap_lang Require Import lib.par proofmode notation.
From solutions Require Import ex_03_spinlock.
(** The program as a heap-lang expression. We use the heap-lang [par] module for (** The program as a heap-lang expression. We use the heap-lang [par] module for
parallel composition. *) parallel composition. *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment