Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Iris
Commits
bbec6617
Commit
bbec6617
authored
Jun 16, 2016
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Fix some Params instances.
parent
cca375a0
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
8 additions
and
3 deletions
+8
-3
heap_lang/heap.v
heap_lang/heap.v
+4
-0
program_logic/auth.v
program_logic/auth.v
+3
-3
program_logic/sts.v
program_logic/sts.v
+1
-0
No files found.
heap_lang/heap.v
View file @
bbec6617
...
@@ -36,7 +36,11 @@ Section definitions.
...
@@ -36,7 +36,11 @@ Section definitions.
Global
Instance
heap_ctx_persistent
N
:
PersistentP
(
heap_ctx
N
).
Global
Instance
heap_ctx_persistent
N
:
PersistentP
(
heap_ctx
N
).
Proof
.
apply
_
.
Qed
.
Proof
.
apply
_
.
Qed
.
End
definitions
.
End
definitions
.
Typeclasses
Opaque
heap_ctx
heap_mapsto
.
Typeclasses
Opaque
heap_ctx
heap_mapsto
.
Instance
:
Params
(@
heap_inv
)
1
.
Instance
:
Params
(@
heap_mapsto
)
4
.
Instance
:
Params
(@
heap_ctx
)
2
.
Notation
"l ↦{ q } v"
:
=
(
heap_mapsto
l
q
v
)
Notation
"l ↦{ q } v"
:
=
(
heap_mapsto
l
q
v
)
(
at
level
20
,
q
at
level
50
,
format
"l ↦{ q } v"
)
:
uPred_scope
.
(
at
level
20
,
q
at
level
50
,
format
"l ↦{ q } v"
)
:
uPred_scope
.
...
...
program_logic/auth.v
View file @
bbec6617
...
@@ -41,9 +41,9 @@ Section definitions.
...
@@ -41,9 +41,9 @@ Section definitions.
End
definitions
.
End
definitions
.
Typeclasses
Opaque
auth_own
auth_ctx
.
Typeclasses
Opaque
auth_own
auth_ctx
.
Instance
:
Params
(@
auth_inv
)
6
.
Instance
:
Params
(@
auth_inv
)
5
.
Instance
:
Params
(@
auth_own
)
6
.
Instance
:
Params
(@
auth_own
)
5
.
Instance
:
Params
(@
auth_ctx
)
7
.
Instance
:
Params
(@
auth_ctx
)
6
.
Section
auth
.
Section
auth
.
Context
`
{
AuthI
:
authG
Λ
Σ
A
}.
Context
`
{
AuthI
:
authG
Λ
Σ
A
}.
...
...
program_logic/sts.v
View file @
bbec6617
...
@@ -46,6 +46,7 @@ Section definitions.
...
@@ -46,6 +46,7 @@ Section definitions.
Global
Instance
sts_ctx_persistent
N
φ
:
PersistentP
(
sts_ctx
N
φ
).
Global
Instance
sts_ctx_persistent
N
φ
:
PersistentP
(
sts_ctx
N
φ
).
Proof
.
apply
_
.
Qed
.
Proof
.
apply
_
.
Qed
.
End
definitions
.
End
definitions
.
Typeclasses
Opaque
sts_own
sts_ownS
sts_ctx
.
Typeclasses
Opaque
sts_own
sts_ownS
sts_ctx
.
Instance
:
Params
(@
sts_inv
)
5
.
Instance
:
Params
(@
sts_inv
)
5
.
Instance
:
Params
(@
sts_ownS
)
5
.
Instance
:
Params
(@
sts_ownS
)
5
.
...
...
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