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

export lock from spin_lock

parent 7b4c8e1e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris_heap_lang/lib/spin_lock.v
+ 1
− 1
View file @ cc54c166
...@@ -3,7 +3,7 @@ From iris.proofmode Require Import proofmode. ...@@ -3,7 +3,7 @@ From iris.proofmode Require Import proofmode.
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import lock. From iris.heap_lang.lib Require Export lock.
From iris.prelude Require Import options. From iris.prelude Require Import options.
Local Definition newlock : val := λ: <>, ref #false. Local Definition newlock : val := λ: <>, ref #false.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment