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
Iris
Commits
c800ca9c
Commit
c800ca9c
authored
Nov 21, 2017
by
Ralf Jung
Browse files
Merge branch 'master' of
https://gitlab.mpi-sws.org/FP/iris-coq
parents
c984a2bc
e824f642
Pipeline
#5491
passed with stages
in 5 minutes and 58 seconds
Changes
5
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
opam
View file @
c800ca9c
...
...
@@ -12,5 +12,5 @@ remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { >= "8.6.1" & < "8.8~" }
"coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
"coq-stdpp" { (= "dev.2017-11-
18
.0") | (= "dev") }
"coq-stdpp" { (= "dev.2017-11-
20
.0") | (= "dev") }
]
theories/algebra/ofe.v
View file @
c800ca9c
...
...
@@ -1061,6 +1061,7 @@ Inductive later (A : Type) : Type := Next { later_car : A }.
Add
Printing
Constructor
later
.
Arguments
Next
{
_
}
_
.
Arguments
later_car
{
_
}
_
.
Instance
:
Params
(@
Next
)
1
.
Section
later
.
Context
{
A
:
ofeT
}.
...
...
theories/algebra/sts.v
View file @
c800ca9c
...
...
@@ -79,7 +79,7 @@ Qed.
Global
Instance
up_set_preserving
:
Proper
((
⊆
)
==>
flip
(
⊆
)
==>
(
⊆
))
up_set
.
Proof
.
intros
S1
S2
HS
T1
T2
HT
.
rewrite
/
up_set
.
f_equiv
=>
//
s1
s2
Hs
.
by
apply
up_preserving
.
f_equiv
=>
//
s1
s2
.
by
apply
up_preserving
.
Qed
.
Global
Instance
up_set_proper
:
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
up_set
.
Proof
.
...
...
theories/base_logic/lib/saved_prop.v
View file @
c800ca9c
...
...
@@ -21,7 +21,7 @@ Definition saved_anything_own `{savedAnythingG Σ F}
(
γ
:
gname
)
(
x
:
F
(
iProp
Σ
))
:
iProp
Σ
:
=
own
γ
(
to_agree
$
(
cFunctor_map
F
(
iProp_fold
,
iProp_unfold
)
x
)).
Typeclasses
Opaque
saved_anything_own
.
Instance
:
Params
(@
saved_anything_own
)
3
.
Instance
:
Params
(@
saved_anything_own
)
4
.
Section
saved_anything
.
Context
`
{
savedAnythingG
Σ
F
}.
...
...
theories/base_logic/lib/wsat.v
View file @
c800ca9c
...
...
@@ -23,6 +23,7 @@ Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
own
invariant_name
(
◯
{[
i
:
=
invariant_unfold
P
]}).
Arguments
ownI
{
_
_
}
_
_
%
I
.
Typeclasses
Opaque
ownI
.
Instance
:
Params
(@
invariant_unfold
)
1
.
Instance
:
Params
(@
ownI
)
3
.
Definition
ownE
`
{
invG
Σ
}
(
E
:
coPset
)
:
iProp
Σ
:
=
...
...
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