Commit d7aa1f6e authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 9db1d7a4
Pipeline #20678 passed with stage
in 16 minutes and 27 seconds
...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [ depends: [
"coq-iris" { (= "dev.2019-09-19.0.ca3f9d11") | (= "dev") } "coq-iris" { (= "dev.2019-09-19.3.aa7871c7") | (= "dev") }
] ]
...@@ -42,7 +42,7 @@ Class ironInvG (Σ : gFunctors) := IronInvG { ...@@ -42,7 +42,7 @@ Class ironInvG (Σ : gFunctors) := IronInvG {
fcinv_inG :> inG Σ (frac_authR ufracR); fcinv_inG :> inG Σ (frac_authR ufracR);
}. }.
Notation ironProp Σ := (fracPred (iProp Σ)). Notation ironProp Σ := (fracPred (iProp Σ)).
Notation ironPropC Σ := (fracPredO (iProp Σ)). Notation ironPropO Σ := (fracPredO (iPropO Σ)).
Notation ironPropI Σ := (fracPredI (uPredI (iResUR Σ))). Notation ironPropI Σ := (fracPredI (uPredI (iResUR Σ))).
Notation ironPropSI Σ := (fracPredSI (uPredSI (iResUR Σ))). Notation ironPropSI Σ := (fracPredSI (uPredSI (iResUR Σ))).
......
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