From 2c64b5512f38450c23a44e75727036e3b964bdfd Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Wed, 14 Sep 2016 12:55:19 +0200
Subject: [PATCH] Correct the name gmap_persistent -> gset_persistent
---
algebra/gset.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/algebra/gset.v b/algebra/gset.v
index 2d4addaf0..a00ced785 100644
--- a/algebra/gset.v
+++ b/algebra/gset.v
@@ -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.
--
GitLab