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

Bump Iris (Loc module).

parent 87916dfb
No related branches found
No related tags found
No related merge requests found
Pipeline #81731 failed
Hide whitespace changes
Inline Side-by-side
coq-reloc.opam
+ 1
− 1
View file @ 32081959
...@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues" ...@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git" dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
depends: [ depends: [
"coq-iris-heap-lang" { (= "dev.2023-03-09.0.f91e8eab") | (= "dev") } "coq-iris-heap-lang" { (= "dev.2023-03-17.1.a7a250e6") | (= "dev") }
"coq-autosubst" { = "dev" } "coq-autosubst" { = "dev" }
] ]
......
theories/logic/spec_rules.v
+ 1
− 1
View file @ 32081959
...@@ -154,7 +154,7 @@ Section rules. ...@@ -154,7 +154,7 @@ Section rules.
rewrite to_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro. rewrite to_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
eapply rtc_r, step_insert_no_fork; eauto. eapply rtc_r, step_insert_no_fork; eauto.
rewrite -state_init_heap_singleton. eapply AllocNS; first by lia. rewrite -state_init_heap_singleton. eapply AllocNS; first by lia.
intros. assert (i = 0) as -> by lia. by rewrite loc_add_0. intros. assert (i = 0) as -> by lia. by rewrite Loc.add_0.
Qed. Qed.
Lemma step_load E j K l q v: Lemma step_load E j K l q v:
......
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