Skip to content
Snippets Groups Projects

make wp_par usable

Merged Ralf Jung requested to merge ralf/wp_par into master
Files
6
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation par.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
(** Nondeterminism and Speculation:
Loading