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
Janno
iris-coq
Commits
4417e093
Commit
4417e093
authored
May 29, 2018
by
Ralf Jung
Browse files
move comment closer to where it is exploited
parent
e60b556f
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/algebra/cmra.v
View file @
4417e093
...
...
@@ -170,11 +170,11 @@ Hint Mode IdFree + ! : typeclass_instances.
Instance
:
Params
(@
IdFree
)
1
.
(** * CMRAs whose core is total *)
(** The function [core] may return a dummy when used on CMRAs without total
core. *)
Class
CmraTotal
(
A
:
cmraT
)
:
=
cmra_total
(
x
:
A
)
:
is_Some
(
pcore
x
).
Hint
Mode
CmraTotal
!
:
typeclass_instances
.
(** The function [core] returns a dummy when used on CMRAs without total
core. *)
Class
Core
(
A
:
Type
)
:
=
core
:
A
→
A
.
Hint
Mode
Core
!
:
typeclass_instances
.
Instance
:
Params
(@
core
)
2
.
...
...
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