Commit 0c1aa0a0 authored by Ralf Jung's avatar Ralf Jung

bump Iris for LitErased -> LitPoison rename

parent 034e63b6
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2019-10-25.0.bbd38120") | (= "dev") }
"coq-iris" { (= "dev.2019-11-02.1.9d4613fc") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -29,7 +29,7 @@ Fixpoint erase_expr (e : expr) : expr :=
| Store e1 e2 => Store (erase_expr e1) (erase_expr e2)
| CmpXchg e0 e1 e2 => CmpXchg (erase_expr e0) (erase_expr e1) (erase_expr e2)
| FAA e1 e2 => FAA (erase_expr e1) (erase_expr e2)
| NewProph => ((λ: <>, #LitErased)%V #())
| NewProph => ((λ: <>, #LitPoison)%V #())
| Resolve e0 e1 e2 => Fst (Fst (erase_expr e0, erase_expr e1, erase_expr e2))
end
with
......@@ -38,7 +38,7 @@ erase_val (v : val) : val :=
| LitV l =>
LitV
match l with
| LitProphecy p => LitErased
| LitProphecy p => LitPoison
| _ => l
end
| RecV f x e => RecV f x (erase_expr e)
......
Markdown is supported
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