diff --git a/theories/base_logic/bupd_alt.v b/theories/base_logic/bupd_alt.v
index b40031111a65e3f0ace2d9af73449eb8bf4588a9..c058493a20cdeb382bba742f73368465aa5437bf 100644
--- a/theories/base_logic/bupd_alt.v
+++ b/theories/base_logic/bupd_alt.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Export base_logic.
 From iris Require Import options.
 
-(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+(* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
 Set Default Proof Using "Type*".
 
 (** This file contains an alternative version of basic updates, that is
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/theories/base_logic/lib/fancy_updates_from_vs.v
index 4d3654f6889fa2b3b2cb15c7f9d0deb8cd3eff2e..f1c0ccc101bbd13b47ce0240234107100cfd8ca1 100644
--- a/theories/base_logic/lib/fancy_updates_from_vs.v
+++ b/theories/base_logic/lib/fancy_updates_from_vs.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Export base_logic.
 From iris Require Import options.
 
-(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+(* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
 Set Default Proof Using "Type*".
 
 Section fupd.
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index a9710b744658df236134877e46daa011045bc0d6..57a016d07b2ca80e98939edfe5c5b6b29ba6ab65 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -2,7 +2,7 @@ From iris.bi Require Export derived_connectives.
 From iris.algebra Require Import monoid.
 From iris Require Import options.
 
-(* The sections add [BiAffine] and the like, which is only picked up with "Type"*. *)
+(* The sections add [BiAffine] and the like, which is only picked up with [Type*]. *)
 Set Default Proof Using "Type*".
 
 (** Naming schema for lemmas about modalities:
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 8a8374852ddc9e33aa3710498ec5d2477de9912e..4a70ddb3b2027ca569efd5067e2141cf429f9a30 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -3,7 +3,7 @@ From iris.bi Require Import plainly updates internal_eq.
 From iris.algebra Require Import monoid.
 From iris Require Import options.
 
-(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+(* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
 Set Default Proof Using "Type*".
 
 Class Embed (A B : Type) := embed : A → B.