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

fix for std++ update

parent dde08018
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/program_logic/language.v
+ 1
− 1
View file @ 82bd9f1d
......@@ -198,7 +198,7 @@ Section language.
Proof.
intros Ht [e1 σ1' e2 σ2' efs tl tr ?? Hstep]; simplify_eq/=.
move: Ht; rewrite -Permutation_middle (symmetry_iff (≡ₚ)).
intros (tl'&tr'&->&Ht)%Permutation_cons_inv.
intros (tl'&tr'&->&Ht)%Permutation_cons_inv_r.
exists (tl' ++ e2 :: tr' ++ efs); split; [|by econstructor].
by rewrite -!Permutation_middle !assoc_L Ht.
Qed.
......
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