diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index dd7f9f7e5ceab57cf70320afcf94ea91d80c994b..72c3ea3e31e2fe3fc2e5b651e1dc8f8b4deee30c 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -211,9 +211,9 @@ Proof. apply pure_soundness. Qed.
Lemma later_soundness P : bi_emp_valid (▷ P) → bi_emp_valid P.
Proof. apply later_soundness. Qed.
+(** See [derived.v] for a similar soundness result for basic updates. *)
End restate.
-(** See [derived.v] for the version for basic updates. *)
(** New unseal tactic that also unfolds the BI layer.
This is used by [base_logic.double_negation].