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
Dan Frumin
iris-coq
Commits
aa6c43a2
Commit
aa6c43a2
authored
Jun 15, 2016
by
Robbert Krebbers
Browse files
Make additional carrier fields in structures anonymous.
parent
97dc4393
Changes
2
Hide whitespace changes
Inline
Side-by-side
algebra/cmra.v
View file @
aa6c43a2
...
@@ -63,7 +63,7 @@ Structure cmraT := CMRAT' {
...
@@ -63,7 +63,7 @@ Structure cmraT := CMRAT' {
cmra_validN
:
ValidN
cmra_car
;
cmra_validN
:
ValidN
cmra_car
;
cmra_cofe_mixin
:
CofeMixin
cmra_car
;
cmra_cofe_mixin
:
CofeMixin
cmra_car
;
cmra_mixin
:
CMRAMixin
cmra_car
;
cmra_mixin
:
CMRAMixin
cmra_car
;
cmra_car
'
:
Type
_
:
Type
}
.
}
.
Arguments
CMRAT
'
_
{
_
_
_
_
_
_
_
}
_
_
_.
Arguments
CMRAT
'
_
{
_
_
_
_
_
_
_
}
_
_
_.
Notation
CMRAT
A
m
m
'
:=
(
CMRAT
'
A
m
m
'
A
).
Notation
CMRAT
A
m
m
'
:=
(
CMRAT
'
A
m
m
'
A
).
...
@@ -165,7 +165,7 @@ Structure ucmraT := UCMRAT' {
...
@@ -165,7 +165,7 @@ Structure ucmraT := UCMRAT' {
ucmra_cofe_mixin
:
CofeMixin
ucmra_car
;
ucmra_cofe_mixin
:
CofeMixin
ucmra_car
;
ucmra_cmra_mixin
:
CMRAMixin
ucmra_car
;
ucmra_cmra_mixin
:
CMRAMixin
ucmra_car
;
ucmra_mixin
:
UCMRAMixin
ucmra_car
;
ucmra_mixin
:
UCMRAMixin
ucmra_car
;
ucmra_car
'
:
Type
;
_
:
Type
;
}
.
}
.
Arguments
UCMRAT
'
_
{
_
_
_
_
_
_
_
_
}
_
_
_
_.
Arguments
UCMRAT
'
_
{
_
_
_
_
_
_
_
_
}
_
_
_
_.
Notation
UCMRAT
A
m
m
'
m
''
:=
(
UCMRAT
'
A
m
m
'
m
''
A
).
Notation
UCMRAT
A
m
m
'
m
''
:=
(
UCMRAT
'
A
m
m
'
m
''
A
).
...
...
algebra/cofe.v
View file @
aa6c43a2
...
@@ -64,7 +64,7 @@ Structure cofeT := CofeT' {
...
@@ -64,7 +64,7 @@ Structure cofeT := CofeT' {
cofe_dist
:
Dist
cofe_car
;
cofe_dist
:
Dist
cofe_car
;
cofe_compl
:
Compl
cofe_car
;
cofe_compl
:
Compl
cofe_car
;
cofe_mixin
:
CofeMixin
cofe_car
;
cofe_mixin
:
CofeMixin
cofe_car
;
cofe_car
'
:
Type
_
:
Type
}
.
}
.
Arguments
CofeT
'
_
{
_
_
_
}
_
_.
Arguments
CofeT
'
_
{
_
_
_
}
_
_.
Notation
CofeT
A
m
:=
(
CofeT
'
A
m
A
).
Notation
CofeT
A
m
:=
(
CofeT
'
A
m
A
).
...
...
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