Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
examples
Commits
9bad5ed7
Commit
9bad5ed7
authored
Dec 14, 2017
by
Ralf Jung
Browse files
fix building with coq 8.6.1
parent
90d27fc2
Pipeline
#5935
passed with stage
in 10 minutes and 12 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/logrel/F_mu_ref_conc/examples/counter.v
View file @
9bad5ed7
...
...
@@ -126,8 +126,8 @@ Section CG_Counter.
iIntros
(
HNE
)
"[#Hspec [Hx [Hl Hj]]]"
.
iMod
(
steps_with_lock
_
_
j
K
_
_
_
_
UnitV
UnitV
_
_
with
"[Hj Hx Hl]"
)
as
"Hj"
;
last
done
.
-
iIntros
(
K'
)
"[#Hspec
[
Hx
Hj]
]"
.
iApply
steps_CG_increment
;
first
done
.
iFrame
.
iSplitR
;
trivial
.
-
iIntros
(
K'
)
"[#Hspec Hx
j
]"
.
iApply
steps_CG_increment
;
first
done
.
iFrame
.
trivial
.
-
by
iFrame
"Hspec Hj Hx"
.
Unshelve
.
all
:
trivial
.
Qed
.
...
...
theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
View file @
9bad5ed7
...
...
@@ -138,8 +138,8 @@ Section CG_Stack.
intros
HNE
.
iIntros
"[#Hspec [Hx [Hl Hj]]]"
.
unfold
CG_locked_push
.
iMod
(
steps_with_lock
_
_
j
K
_
_
_
_
UnitV
_
_
_
with
"[Hj Hx Hl]"
)
as
"Hj"
;
last
done
.
-
iIntros
(
K'
)
"[#Hspec
[
Hx
Hj]
]"
.
iApply
steps_CG_push
;
first
done
.
iFrame
.
iSplitR
;
trivial
.
-
iIntros
(
K'
)
"[#Hspec Hx
j
]"
.
iApply
steps_CG_push
;
first
done
.
iFrame
.
trivial
.
-
iFrame
"Hspec Hj Hx"
;
trivial
.
Unshelve
.
all
:
trivial
.
Qed
.
...
...
@@ -272,8 +272,8 @@ Section CG_Stack.
iIntros
(
HNE
)
"[#Hspec [Hx [Hl Hj]]]"
.
unfold
CG_locked_pop
.
iMod
(
steps_with_lock
_
_
j
K
_
_
_
_
(
InjRV
w
)
UnitV
_
_
with
"[Hj Hx Hl]"
)
as
"Hj"
;
last
done
.
-
iIntros
(
K'
)
"[#Hspec
[
Hx
Hj]
]"
.
iApply
steps_CG_pop_suc
;
first
done
.
iFrame
.
by
iSplitR
.
-
iIntros
(
K'
)
"[#Hspec Hx
j
]"
.
iApply
steps_CG_pop_suc
;
first
done
.
by
iFrame
.
-
iFrame
"Hspec Hj Hx"
;
trivial
.
Unshelve
.
all
:
trivial
.
Qed
.
...
...
@@ -287,8 +287,8 @@ Section CG_Stack.
iIntros
(
HNE
)
"[#Hspec [Hx [Hl Hj]]]"
.
unfold
CG_locked_pop
.
iMod
(
steps_with_lock
_
_
j
K
_
_
_
_
(
InjLV
UnitV
)
UnitV
_
_
with
"[Hj Hx Hl]"
)
as
"Hj"
;
last
done
.
-
iIntros
(
K'
)
"[#Hspec
[
Hx
Hj]
] /="
.
iApply
steps_CG_pop_fail
;
first
done
.
iFrame
.
by
iSplitR
.
-
iIntros
(
K'
)
"[#Hspec Hx
j
] /="
.
iApply
steps_CG_pop_fail
;
first
done
.
by
iFrame
.
-
iFrame
"Hspec Hj Hx"
;
trivial
.
Unshelve
.
all
:
trivial
.
Qed
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment