diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v index bc81eba1ede44385c729f7d62fa6c19a79ac5c80..a4dd54d35006d3604f3c78eaeae619f75ff9f09f 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) :=