Skip to content
Snippets Groups Projects
Commit 3c32ead9 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Fix build (change of names).

parent cc4741b4
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
theories/lang/heap.v
+ 1
− 1
View file @ 3c32ead9
...@@ -144,7 +144,7 @@ Section heap. ...@@ -144,7 +144,7 @@ Section heap.
Lemma heap_mapsto_agree l q1 q2 v1 v2 : Lemma heap_mapsto_agree l q1 q2 v1 v2 :
l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝. l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
Proof. Proof.
rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid. rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
eapply pure_elim; [done|]=> /auth_own_valid /=. eapply pure_elim; [done|]=> /auth_own_valid /=.
rewrite op_singleton pair_op singleton_valid. case. rewrite op_singleton pair_op singleton_valid. case.
rewrite /= to_agree_comp_valid=>? Heq. fold_leibniz. eauto. rewrite /= to_agree_comp_valid=>? Heq. fold_leibniz. eauto.
......
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