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

Bump Iris.

parent 1f8f00d8
No related branches found
No related tags found
No related merge requests found
Pipeline #
...@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"] ...@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [ depends: [
"coq-iris" { (= "dev.2017-11-07.2") | (= "dev") } "coq-iris" { (= "dev.2017-11-11.0") | (= "dev") }
] ]
...@@ -43,7 +43,7 @@ Module Type lifetime_sig. ...@@ -43,7 +43,7 @@ Module Type lifetime_sig.
Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : uPred_scope. Notation "&{ κ , i }" := (idx_bor κ i) (format "&{ κ , i }") : uPred_scope.
Infix "⊑" := lft_incl (at level 70) : uPred_scope. Infix "⊑" := lft_incl (at level 70) : uPred_scope.
Infix "⊓" := lft_intersect (at level 40) : C_scope. Infix "⊓" := lft_intersect (at level 40) : stdpp_scope.
Section properties. Section properties.
Context `{invG, lftG Σ}. Context `{invG, lftG Σ}.
......
...@@ -20,7 +20,7 @@ End lft_notation. ...@@ -20,7 +20,7 @@ End lft_notation.
Definition static : lft := ( : gmultiset _). Definition static : lft := ( : gmultiset _).
Definition lft_intersect (κ κ' : lft) : lft := κ κ'. Definition lft_intersect (κ κ' : lft) : lft := κ κ'.
Infix "⊓" := lft_intersect (at level 40) : C_scope. Infix "⊓" := lft_intersect (at level 40) : stdpp_scope.
Inductive bor_state := Inductive bor_state :=
| Bor_in | Bor_in
......
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