From d23ae90d3395dc2bcabb5857f8ffe232fa6c9337 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 19 Jan 2018 11:28:51 +0100
Subject: [PATCH] Update Coq bug in comment.
---
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 a7a408568..25e1a364b 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')
| _ =>
--
GitLab