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 2c64b551
Prev Next
Show latest version
1 file
+ 1
− 1
Compare changes
  • Side-by-side
  • Inline
algebra/gset.v
+ 1
− 1
@@ -54,7 +54,7 @@ Section gset.
intros mZ _. rewrite !gset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX.
Qed.
Global Instance gmap_persistent X : Persistent X.
Global Instance gset_persistent X : Persistent X.
Proof. by apply persistent_total; rewrite gset_core_self. Qed.
End gset.