Skip to content
Snippets Groups Projects
Commit 80731928 authored by Simcha van Collem's avatar Simcha van Collem
Browse files

Explictly name variables, such that CI won't fail when we iRevert them

parent 942d311a
No related branches found
No related tags found
No related merge requests found
Pipeline #74183 passed
......@@ -158,7 +158,7 @@ Section general.
( x y, Persistent (R x y))
x y, Persistent (bi_rtc R x y).
Proof.
intros. rewrite /Persistent.
intros ? x y. rewrite /Persistent.
iRevert (x). iApply bi_rtc_ind_l; first solve_proper.
iIntros "!>" (x) "[#Heq | (%x' & #Hxx' & #Hx'y)]".
{ iRewrite "Heq". iApply bi_rtc_refl. }
......@@ -267,7 +267,7 @@ Section general.
( x y, Persistent (R x y))
x y, Persistent (bi_tc R x y).
Proof.
intros. rewrite /Persistent.
intros ? x y. rewrite /Persistent.
iRevert (x). iApply bi_tc_ind_l; first solve_proper.
iIntros "!# %x [#H|(%x'&#?&#?)] !>"; first by iApply bi_tc_once.
by iApply bi_tc_l.
......
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