Skip to content
Snippets Groups Projects

Make the elements of gset persistent by changing the core

Merged Make the elements of gset persistent by changing the core
amintimany/iris-coq:master into master
1 unresolved thread
Merged Amin Timany requested to merge amintimany/iris-coq:master into master
1 unresolved thread
Viewing commit bfad9bff
Prev
Show latest version
1 file
+ 1
− 1
Compare changes
  • Side-by-side
  • Inline
algebra/gset.v
+ 1
− 1
@@ -32,7 +32,7 @@ Section gset.
@@ -32,7 +32,7 @@ Section gset.
- solve_proper.
- solve_proper.
- intros X1 X2 X3. by rewrite !gset_op_union assoc_L.
- intros X1 X2 X3. by rewrite !gset_op_union assoc_L.
- intros X1 X2. by rewrite !gset_op_union comm_L.
- intros X1 X2. by rewrite !gset_op_union comm_L.
- intros X. by rewrite gset_op_union gset_core_self union_idemp_L.
- intros X. by rewrite gset_core_self idemp_L.
Qed.
Qed.
Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.
Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.