diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 3b93a6e656c40babf0959b839bacbf404c0b456a..713caba78c85c41685b4bc3b9e152700c8763bad 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -217,7 +217,7 @@ End restate.
 
 
 (** New unseal tactic that also unfolds the BI layer.
-    This is used by [base_logic.double_negation].
+    This is used by [base_logic.bupd_alt].
     TODO: Can we get rid of this? *)
 Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
   unfold bi_emp; simpl; unfold sbi_emp; simpl;