Commit 9dd4d1ea authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'paolo/fix-461' into 'master'

Add testcase for #461

See merge request !798
parents 2ce5597c 9851ef8d
Pipeline #66135 passed with stage
in 13 minutes and 19 seconds
Require Import stdpp.coPset.
Require Import
Require Import
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Import proofmode notation atomic_heap.
......@@ -5,6 +8,14 @@ From iris.prelude Require Import options.
Unset Mangle Names.
Section definition.
Context `{BiFUpd PROP} {TA TB : tele} (Eo Ei : coPset).
Definition AU_tele_quantify_iris : Prop :=
(TA TB : tele) (α : TA PROP) (β Φ : TA TB PROP),
atomic_update Eo Ei α β Φ.
End definition.
Section tests.
Context `{!heapGS Σ} {aheap: atomic_heap Σ}.
Import atomic_heap.notation.
Supports Markdown
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