From 2eb91537650306f7fb2dc1df9599b0a201d32e59 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Jan 2018 14:45:52 -0800
Subject: [PATCH] Fix bug reference.

---
 theories/proofmode/tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index bc81eba1e..a4dd54d35 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -390,7 +390,7 @@ resolved at arbitrary moments. It seems that tactics like `apply`, `split` and
 triggered too eagerly, this tactic uses `refine` at various places instead of
 `apply`.
 
-TODO: Investigate what really is going on. Is there a related to Cog bug #5752?
+TODO: Investigate what really is going on. Is there a related to Cog bug #4969?
 When should holes in an `open_constr` be resolved?
 *)
 Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
-- 
GitLab