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
Jonas Kastberg
iris
Commits
e824f642
Commit
e824f642
authored
Nov 20, 2017
by
Robbert Krebbers
Browse files
Correct some `Params` instances.
parent
7a04946d
Changes
3
Hide whitespace changes
Inline
Side-by-side
theories/algebra/ofe.v
View file @
e824f642
...
...
@@ -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/base_logic/lib/saved_prop.v
View file @
e824f642
...
...
@@ -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 @
e824f642
...
...
@@ -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