Skip to content
Snippets Groups Projects
Commit c718ba6f authored by Ralf Jung's avatar Ralf Jung
Browse files

fix sed fubar

parent 99d3d681
No related branches found
No related tags found
No related merge requests found
Pipeline #34134 passed
...@@ -71,7 +71,7 @@ Section cnt_model. ...@@ -71,7 +71,7 @@ Section cnt_model.
iPureIntro. revert Hfoo. iPureIntro. revert Hfoo.
rewrite -auth_frag_op -Some_op -pair_op. rewrite -auth_frag_op -Some_op -pair_op.
rewrite auth_frag_valid Some_valid. rewrite auth_frag_valid Some_valid.
by intros [_ foo%to_agree_op_inv_L']%pair_valid. by intros [_ foo%to_agree_op_inv_L]%pair_valid.
Qed. Qed.
Lemma cnt_agree_2 γ q n m : Lemma cnt_agree_2 γ q n m :
......
...@@ -142,7 +142,7 @@ Section mapsto. ...@@ -142,7 +142,7 @@ Section mapsto.
rewrite -pair_op singleton_op right_id -pair_op. rewrite -pair_op singleton_op right_id -pair_op.
move=> [_ Hv]. move:Hv => /=. move=> [_ Hv]. move:Hv => /=.
rewrite singleton_valid. rewrite singleton_valid.
by move=> [_] /to_agree_op_inv_L' [->]. by move=> [_] /to_agree_op_inv_L [->].
Qed. Qed.
Lemma mapstoS_valid l q v : l {q} v -∗ q. Lemma mapstoS_valid l q v : l {q} v -∗ q.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment