Commit d23ae90d authored by Robbert Krebbers's avatar Robbert Krebbers

Update Coq bug in comment.

parent 26864df4
Pipeline #6290 passed with stages
in 13 minutes and 12 seconds
......@@ -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')
| _ =>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment