Commit 996a7db5 authored by Ralf Jung's avatar Ralf Jung

fix for Iris axiom change

parent 24c4899b
......@@ -127,7 +127,7 @@ Next Obligation.
by apply HR.
- intros P Q H h. apply H.
- auto.
- unfold hpersistently, hempty. intros P h _. auto.
- unfold hpersistently, hempty. intros h _. auto.
- auto.
- auto.
- intros P Q h. replace (hpersistently P) with (\[P heap_empty] \* \Top).
......
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