diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index dad2afd87f00f1b0bfdf3d80894886fd76e93676..22ece1b62360aa2cc02b921d35300e691ef53bdf 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1,2 +1,4 @@
 From iris.proofmode Require Export ltac_tactics.
+(* This [Require Import] is not a no-op: it exports typeclass instances from
+these files. *)
 From iris.proofmode Require Import class_instances_bi class_instances_sbi frame_instances modality_instances.