Skip to content
Snippets Groups Projects
Commit f6d4980f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Compat with iris/stdpp!309.

parent 7fc6440b
Branches robbert/sprop
No related tags found
No related merge requests found
Pipeline #53197 failed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/typing/soundness.v
+ 0
− 1
View file @ f6d4980f
...@@ -53,7 +53,6 @@ Section type_soundness. ...@@ -53,7 +53,6 @@ Section type_soundness.
{ by rewrite /elctx_interp /=. } { by rewrite /elctx_interp /=. }
{ rewrite /llctx_interp /=. iSplit; last done. iExists ϝ. { rewrite /llctx_interp /=. iSplit; last done. iExists ϝ.
rewrite /= left_id. iSplit; first done. rewrite /= left_id. iSplit; first done.
rewrite decide_True //.
by iDestruct "Hϝ" as "[$ #$]". } by iDestruct "Hϝ" as "[$ #$]". }
rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _". rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
inv_vec args. iIntros (x) "_ /=". by wp_lam. inv_vec args. iIntros (x) "_ /=". by wp_lam.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment