From 196494320e16ae96238b2845a1c1d6e8607aad71 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 27 Nov 2017 09:24:14 +0100
Subject: [PATCH] Fix typo.

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

diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 3f65239d3..814bf3224 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -93,7 +93,7 @@ Section frac_auth.
     IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯!{q} a) (◯!{q1} a1) (◯!{q2} a2).
   Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
 
-  Global Instance is_op_frac_auth_persistent (q q1 q2 : frac) (a  : A) :
+  Global Instance is_op_frac_auth_core_id (q q1 q2 : frac) (a  : A) :
     CoreId a → IsOp q q1 q2 → IsOp' (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
   Proof.
     rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
-- 
GitLab