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

update dependencies, fix `iIntros ""` not doing `iStartProof` any more.

parent 3a07f8f1
No related branches found
No related tags found
No related merge requests found
Pipeline #90049 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
coq-tutorial-popl20.opam
+ 1
− 1
View file @ 7974fc6e
......@@ -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.2023-05-03.3.85295b18") | (= "dev") }
"coq-iris-heap-lang" { (= "dev.2023-08-04.2.b9e591f8") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
exercises/sem_typed.v
+ 1
− 1
View file @ 7974fc6e
......@@ -91,7 +91,7 @@ Section sem_typed.
Qed.
Lemma env_sem_typed_empty : ⊢ env_sem_typed ∅ ∅.
Proof. iIntros "". by rewrite /env_sem_typed. Qed.
Proof. iStartProof. by rewrite /env_sem_typed. Qed.
Lemma env_sem_typed_empty_l_inv vs : env_sem_typed ∅ vs -∗ ⌜vs = ∅⌝.
Proof. by iIntros "?"; iApply big_sepM2_empty_r. Qed.
End sem_typed.
solutions/sem_typed.v
+ 1
− 1
View file @ 7974fc6e
......@@ -91,7 +91,7 @@ Section sem_typed.
Qed.
Lemma env_sem_typed_empty : ⊢ env_sem_typed ∅ ∅.
Proof. iIntros "". by rewrite /env_sem_typed. Qed.
Proof. iStartProof. by rewrite /env_sem_typed. Qed.
Lemma env_sem_typed_empty_l_inv vs : env_sem_typed ∅ vs -∗ ⌜vs = ∅⌝.
Proof. by iIntros "?"; iApply big_sepM2_empty_r. Qed.
End sem_typed.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment