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

bump Iris, fix build

parent 6d816fc0
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
opam
+ 1
− 1
View file @ dec707da
...@@ -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/igps" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
depends: [ depends: [
"coq-iris" { (= "branch.gen_proofmode.2018-04-05.1") | (= "dev") } "coq-iris" { (= "branch.gen_proofmode.2018-05-18.0.ec4ac846") | (= "dev") }
] ]
theories/fractor.v
+ 0
− 1
View file @ dec707da
...@@ -70,7 +70,6 @@ Section Fractor. ...@@ -70,7 +70,6 @@ Section Fractor.
Proof. Proof.
iIntros "[Info1 Info2]". iIntros "[Info1 Info2]".
iCombine "Info1" "Info2" as "Info". iCombine "Info1" "Info2" as "Info".
rewrite op_singleton pair_op.
iDestruct (own_valid with "Info") as %Valid. iDestruct (own_valid with "Info") as %Valid.
apply singleton_valid in Valid. apply singleton_valid in Valid.
destruct Valid as [_ Valid2]. simpl in Valid2. destruct Valid as [_ Valid2]. simpl in Valid2.
......
theories/persistor.v
+ 1
− 4
View file @ dec707da
...@@ -91,7 +91,7 @@ Section Persistor. ...@@ -91,7 +91,7 @@ Section Persistor.
iDestruct "Per2" as (X2) "[Per2 [#Inv2 #[PerCtx2 PerOwn2]]]". iDestruct "Per2" as (X2) "[Per2 [#Inv2 #[PerCtx2 PerOwn2]]]".
iCombine "PerOwn1" "PerOwn2" as "PerOwn". iCombine "PerOwn1" "PerOwn2" as "PerOwn".
iDestruct (own_valid with "PerOwn") as %Valid. iDestruct (own_valid with "PerOwn") as %Valid.
move: Valid. rewrite op_singleton => /singleton_valid /agree_op_inv Valid. move: Valid => /singleton_valid /agree_op_inv Valid.
apply (inj to_agree) in Valid. setoid_subst. apply (inj to_agree) in Valid. setoid_subst.
iExists X2. iFrame. iFrame "Inv2". by iSplit. iExists X2. iFrame. iFrame "Inv2". by iSplit.
- iIntros "Per". - iIntros "Per".
...@@ -110,7 +110,6 @@ Section Persistor. ...@@ -110,7 +110,6 @@ Section Persistor.
iDestruct "P2" as (X2) "(P2 & #Inv2 & #PC2 & #oP2)". iDestruct "P2" as (X2) "(P2 & #Inv2 & #PC2 & #oP2)".
iCombine "oP1" "oP2" as "oP". iCombine "oP1" "oP2" as "oP".
iDestruct (own_valid with "oP") as %Valid. iDestruct (own_valid with "oP") as %Valid.
rewrite op_singleton in Valid.
apply singleton_valid, agree_op_inv, (inj to_agree) in Valid. setoid_subst. apply singleton_valid, agree_op_inv, (inj to_agree) in Valid. setoid_subst.
iExists X2. iFrame "P1 P2 Inv1 oP1 PC1". iExists X2. iFrame "P1 P2 Inv1 oP1 PC1".
Qed. Qed.
...@@ -124,7 +123,6 @@ Section Persistor. ...@@ -124,7 +123,6 @@ Section Persistor.
iDestruct "P2" as (X2) "(P2 & #Inv2 & #PC2 & #oP2)". iDestruct "P2" as (X2) "(P2 & #Inv2 & #PC2 & #oP2)".
iCombine "oP1" "oP2" as "oP". iCombine "oP1" "oP2" as "oP".
iDestruct (own_valid with "oP") as %Valid. iDestruct (own_valid with "oP") as %Valid.
rewrite op_singleton in Valid.
apply singleton_valid, agree_op_inv, (inj to_agree) in Valid. setoid_subst. apply singleton_valid, agree_op_inv, (inj to_agree) in Valid. setoid_subst.
iExists X2. iFrame "P1 P2 Inv2 oP1 PC1". iExists X2. iFrame "P1 P2 Inv2 oP1 PC1".
Qed. Qed.
...@@ -138,7 +136,6 @@ Section Persistor. ...@@ -138,7 +136,6 @@ Section Persistor.
iDestruct "P2" as (X2) "(P2 & #Inv2 & #PC2 & >#oP2)". iDestruct "P2" as (X2) "(P2 & #Inv2 & #PC2 & >#oP2)".
iCombine "oP1" "oP2" as "oP". iCombine "oP1" "oP2" as "oP".
iDestruct (own_valid with "oP") as %Valid. iDestruct (own_valid with "oP") as %Valid.
rewrite op_singleton in Valid.
apply singleton_valid, agree_op_inv, (inj to_agree) in Valid. setoid_subst. apply singleton_valid, agree_op_inv, (inj to_agree) in Valid. setoid_subst.
iExists X2. iModIntro. iFrame "P1 P2 Inv1 oP1 PC1". iExists X2. iModIntro. iFrame "P1 P2 Inv1 oP1 PC1".
Qed. Qed.
......
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