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

update dependencies

parent 68eae2b1
Branches
No related tags found
No related merge requests found
Pipeline #68392 failed
......@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/tutorial-popl20.git"
synopsis: "The Iris tutorial at POPL 2020"
depends: [
"coq-iris-heap-lang" { (= "dev.2021-12-17.0.72485828") | (= "dev") }
"coq-iris-heap-lang" { (= "dev.2022-07-05.1.a32f36a9") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -24,7 +24,7 @@ Lemma sem_gen_type_safety `{!heapGpreS Σ} e σ φ :
( `{!heapGS Σ}, A : sem_ty Σ, ( v, A v -∗ φ v) e : A)
adequate NotStuck e σ (λ v σ, φ v).
Proof.
intros Hty. apply (heap_adequacy Σ NotStuck e σ)=> // ?.
intros Hty. apply (heap_adequacy Σ NotStuck e σ)=> // ??.
specialize (Hty _) as (A & HA & Hty).
iStartProof. iDestruct (Hty $! ) as "#He".
iSpecialize ("He" with "[]"); first by rewrite /env_sem_typed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment