Coq Call 2021 05 12 - coq/coq GitHub Wiki

• May 12th 2021, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Visual debugger in CoqIDE #14252 (Jim). I very much would like to make this available to users in 8.14. Even if it's imperfect or incomplete, I think it's already at a point where it can provide significant value. I would appreciate help identifying reviewers/assignees and expediting their review. There are 4 related PRs: #14220, #14224, #14251 and #14281.

Notes

Kernel and PR #14297: PMP suggests that we are going towards always supplying an explicit type to the kernel rather than letting the kernel infer one among the class of possible ones.

PR #14252 and locating Ltac source text in debugger: some progress, no full conclusion