diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index a7a408568d7a9dac8188eae3b99ae3ab35b1d76b..25e1a364bf56c7a05f8f66cdb71e223073554e63 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -555,7 +555,7 @@ Tactic Notation "iIntoValid" open_constr(t) :=
     | ?P → ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H]
     | ∀ _ : ?T, _ =>
       (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
-      (* This is a workarround for Coq bug #4969. *)
+      (* This is a workarround for Coq bug #6583. *)
       let e := fresh in evar (e:id T);
       let e' := eval unfold e in e in clear e; go (t e')
     | _ =>