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
George Pirlea
Iris
Commits
2c64b551
Commit
2c64b551
authored
Sep 14, 2016
by
Amin Timany
Browse files
Correct the name gmap_persistent -> gset_persistent
parent
3a70097c
Changes
1
Hide whitespace changes
Inline
Side-by-side
algebra/gset.v
View file @
2c64b551
...
...
@@ -54,7 +54,7 @@ Section gset.
intros
mZ
_
.
rewrite
!
gset_opM
=>
HX
.
by
rewrite
(
comm_L
_
X
)
-!
assoc_L
HX
.
Qed
.
Global
Instance
g
map
_persistent
X
:
Persistent
X
.
Global
Instance
g
set
_persistent
X
:
Persistent
X
.
Proof
.
by
apply
persistent_total
;
rewrite
gset_core_self
.
Qed
.
End
gset
.
...
...
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