Commit 087b5c47 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Fix build.

parent 5e9f4d89
Pipeline #7290 passed with stage
in 5 minutes and 27 seconds
From iris.proofmode Require Import tactics.
From iris_examples.logrel.F_mu_ref_conc Require Export rules_binary typing.
From iris.base_logic Require Import namespaces.
(** [newlock = alloc false] *)
Definition newlock : expr := Alloc (# false).
......
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import namespaces.
From iris_examples.logrel.F_mu_ref_conc Require Import examples.lock.
Import uPred.
......
......@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris_examples.logrel.F_mu_ref_conc Require Export rules typing.
From iris.algebra Require Import list.
From iris.base_logic Require Import big_op namespaces invariants.
From iris.base_logic Require Import big_op invariants.
Import uPred.
Definition logN : namespace := nroot .@ "logN".
......
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