Commit b6376268 authored by Dan Frumin's avatar Dan Frumin

U.v doesn't need lib.flock

parent 7e1d0c7c
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris_c.lib Require Import flock locking_heap.
From iris_c.lib Require Import locking_heap.
From iris.proofmode Require Import modalities classes.
Section contents.
Context `{heapG Σ, flockG Σ, locking_heapG Σ}.
Context `{heapG Σ, locking_heapG Σ}.
(** * Unlocking modality *)
Definition U (P : iProp Σ) : iProp Σ :=
Markdown is supported
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