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

update Iris

parent 95f2133a
No related branches found
No related tags found
No related merge requests found
Pipeline #38783 passed
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
depends: [
"coq-iris-heap-lang" { (= "dev.2020-11-13.1.9c531d57") | (= "dev") }
"coq-iris-heap-lang" { (= "dev.2020-11-26.2.03b317f4") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -13,6 +13,8 @@ Section rules.
Implicit Types e t : expr.
Implicit Types v w : val.
Local Existing Instance pure_exec_fill.
(** * Primitive rules *)
(** ([fupd_refines] is defined in [logrel_binary.v]) *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment