Commit c962f679 authored by Ralf Jung's avatar Ralf Jung

update dependencies, fix for heap_lang.lifting rename

parent f28da4e2
......@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/FP/iris-examples.git"
synopsis: "A collection of case studies for Iris"
depends: [
"coq-iris" { (= "dev.2020-05-26.0.e3f87a95") | (= "dev") }
"coq-iris" { (= "dev.2020-05-26.1.d80e7abf") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
"coq-iris-string-ident"
]
......
......@@ -4,7 +4,7 @@
This file: abstract bag specification
*)
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation.
From iris.base_logic.lib Require Export invariants.
From stdpp Require Import gmultiset.
Set Default Proof Using "Type".
......
......@@ -64,7 +64,6 @@ Section proof.
Definition bag_inv (γb : gname) (b : loc) : iProp Σ :=
( ls : list val, b (val_of_list ls) own γb ((1/2)%Qp, to_agree (list_to_set_disj ls)))%I.
Definition is_bag (γb : gname) (x : val) :=
( (lk : val) (b : loc) (γ : gname),
x = PairV #b lk is_lock γ lk (bag_inv γb b))%I.
Definition bag_contents (γb : gname) (X : gmultiset val) : iProp Σ :=
......
From stdpp Require Import namespaces.
From iris.base_logic.lib Require Export gen_inv_heap.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Export proofmode notation.
Set Default Proof Using "Type".
(** A general logically atomic interface for conditional increment. *)
......
From stdpp Require Import namespaces.
From iris.algebra Require Import excl auth list.
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import proofmode atomic_heap.
From iris.heap_lang Require Import proofmode notation atomic_heap.
From iris_examples.logatom.elimination_stack Require spec.
Set Default Proof Using "Type".
......
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import lifting notation.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
(** A general logically atomic interface for a stack. *)
......
......@@ -3,7 +3,7 @@ From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Import atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode atomic_heap.
From iris.heap_lang Require Import proofmode notation atomic_heap.
From iris_examples.logatom.elimination_stack Require Import spec.
Set Default Proof Using "Type".
......
......@@ -3,7 +3,6 @@ From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export invariants proph_map saved_prop.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang.lib Require Import arith diverge.
From iris.heap_lang Require Import proofmode notation par.
From iris_examples.logatom.herlihy_wing_queue Require Import spec.
......
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import lifting notation.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
(** A general logically atomic interface for Herlihy-Wing queues. *)
......
From stdpp Require Import namespaces.
From iris.base_logic.lib Require Export gen_inv_heap.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Export proofmode notation.
Set Default Proof Using "Type".
(** A general logically atomic interface for RDCSS.
......
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import lifting notation.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
(** Specifying snapshots with histories
......
From iris.heap_lang Require Export lifting metatheory.
From iris.heap_lang Require Export derived_laws metatheory.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import notation proofmode.
......
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
(** Specification for a clairvoyant coin. A clairvoyant coin predicts all the
......
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
(** Specification for an eager coin. The coin is only ever tossed once, at the
......
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import auth frac gset gmap excl.
From iris.base_logic Require Export invariants.
From iris.proofmode Require Import tactics.
......
......@@ -2,7 +2,6 @@ From iris.algebra Require Import frac gmap auth.
From iris.base_logic Require Export invariants.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang.lib Require Import par.
From iris.base_logic Require Import cancelable_invariants.
Import uPred.
......
......@@ -2,7 +2,6 @@ From iris.algebra Require Import frac gmap gset excl.
From iris.base_logic Require Export invariants.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang.lib Require Import par.
From iris.base_logic Require Import cancelable_invariants.
Import uPred.
......
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