From cbeb20a2f26a7cef1d1670a64b5ec1de013e5231 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 4 Jan 2017 13:36:18 +0100
Subject: [PATCH] Fix persistent_dup_L.

---
 theories/algebra/cmra.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index c35fac890..c4205ca16 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -575,7 +575,7 @@ Section cmra_leibniz.
   Proof. unfold_leibniz. apply cmra_pcore_dup'. Qed.
 
   (** ** Persistent elements *)
-  Lemma persistent_dup_L x `{!Persistent x} : x ≡ x ⋅ x.
+  Lemma persistent_dup_L x `{!Persistent x} : x = x â‹… x.
   Proof. unfold_leibniz. by apply persistent_dup. Qed.
 
   (** ** Total core *)
-- 
GitLab