diff --git a/theories/si_logic/siprop.v b/theories/si_logic/siprop.v
index 0edf0cb62485b369cbca409faa363f9329279949..2256dc007e4fc4a5acb21a4d1e789f8254f08a3c 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.