diff --git a/iris/hoare.v b/iris/hoare.v
index a52f50f7d180e52a0b4be9801195dd5a0e02102f..018f8858acb68be251540a0b4ec469e85be3e193 100644
--- a/iris/hoare.v
+++ b/iris/hoare.v
@@ -6,9 +6,9 @@ Definition ht {Σ} (E : coPset) (P : iProp Σ)
 Instance: Params (@ht) 2.
 
 Notation "{{ P } } e @ E {{ Q } }" := (ht E P e Q)
-  (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : C_scope.
+  (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : uPred_scope.
 Notation "{{ P } } e @ E {{ Q } }" := (True ⊑ ht E P e Q)
-  (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : type_scope.
+  (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : C_scope.
 
 Section hoare.
 Context {Σ : iParam}.