Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
George Pirlea
Iris
Commits
8271701f
Commit
8271701f
authored
Apr 26, 2019
by
Robbert Krebbers
Browse files
Bump stdpp.
parent
a9031f7f
Changes
2
Hide whitespace changes
Inline
Side-by-side
opam
View file @
8271701f
...
...
@@ -11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-04-2
5
.1.
d6eb24f2
") | (= "dev") }
"coq-stdpp" { (= "dev.2019-04-2
6
.1.
b52e911c
") | (= "dev") }
]
theories/proofmode/frame_instances.v
View file @
8271701f
...
...
@@ -296,14 +296,14 @@ Global Instance make_laterN_default P : MakeLaterN n P (▷^n P) | 100.
Proof
.
by
rewrite
/
MakeLaterN
.
Qed
.
Global
Instance
frame_later
p
R
R'
P
Q
Q'
:
NoBackTrack
(
MaybeIntoLaterN
true
1
R'
R
)
→
TC
NoBackTrack
(
MaybeIntoLaterN
true
1
R'
R
)
→
Frame
p
R
P
Q
→
MakeLaterN
1
Q
Q'
→
Frame
p
R'
(
▷
P
)
Q'
.
Proof
.
rewrite
/
Frame
/
MakeLaterN
/
MaybeIntoLaterN
=>-[->]
<-
<-.
by
rewrite
later_intuitionistically_if_2
later_sep
.
Qed
.
Global
Instance
frame_laterN
p
n
R
R'
P
Q
Q'
:
NoBackTrack
(
MaybeIntoLaterN
true
n
R'
R
)
→
TC
NoBackTrack
(
MaybeIntoLaterN
true
n
R'
R
)
→
Frame
p
R
P
Q
→
MakeLaterN
n
Q
Q'
→
Frame
p
R'
(
▷
^
n
P
)
Q'
.
Proof
.
rewrite
/
Frame
/
MakeLaterN
/
MaybeIntoLaterN
=>-[->]
<-
<-.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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