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
Iris
RefinedC
Commits
3d8fceab
Commit
3d8fceab
authored
May 21, 2021
by
Rodolphe Lepigre
Browse files
Remove useless argument on instance.
parent
2b922cb0
Pipeline
#47046
passed with stage
in 20 minutes and 58 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/typing/intptr.v
View file @
3d8fceab
...
...
@@ -180,7 +180,7 @@ Section programs.
Proof
.
iApply
typed_un_op_wand
.
iApply
intptr_wand_int
.
Qed
.
Global
Instance
typed_un_op_intptr_inst
it
v
l
op
`
{!
Movable
ty
}
:
Global
Instance
typed_un_op_intptr_inst
it
v
l
op
:
TypedUnOpVal
v
(
l
@
intptr
it
)%
I
op
(
IntOp
it
)
:
=
λ
T
,
i2p
(
typed_un_op_intptr
it
v
l
op
T
).
...
...
Write
Preview
Supports
Markdown
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