From 52bfb792e9f25ac3d93dddf1eff41fa57b171040 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 6 Apr 2020 22:28:14 +0200
Subject: [PATCH] =?UTF-8?q?Fix=20typo=20siPropC=20=E2=86=92=20siPropO.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/si_logic/siprop.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/si_logic/siprop.v b/theories/si_logic/siprop.v
index 0edf0cb62..2256dc007 100644
--- a/theories/si_logic/siprop.v
+++ b/theories/si_logic/siprop.v
@@ -33,15 +33,15 @@ Section cofe.
         by trans (Q i);[apply HP|apply HQ].
     - intros n P Q HPQ; split=> i ?; apply HPQ; auto.
   Qed.
-  Canonical Structure siPropC : ofeT := OfeT siProp siProp_ofe_mixin.
+  Canonical Structure siPropO : ofeT := OfeT siProp siProp_ofe_mixin.
 
-  Program Definition siProp_compl : Compl siPropC := λ c,
+  Program Definition siProp_compl : Compl siPropO := λ c,
     {| siProp_holds n := c n n |}.
   Next Obligation.
     intros c n1 n2 ??; simpl in *.
     apply (chain_cauchy c n2 n1); eauto using siProp_closed.
   Qed.
-  Global Program Instance siProp_cofe : Cofe siPropC := {| compl := siProp_compl |}.
+  Global Program Instance siProp_cofe : Cofe siPropO := {| compl := siProp_compl |}.
   Next Obligation.
     intros n c; split=>i ?; symmetry; apply (chain_cauchy c i n); auto.
   Qed.
-- 
GitLab