CoqCS1 bsp

Bug Squashing Party

This page lists a collection of open bugs. If you are working on one of these, please edit the page adding (TAKEN: yourname) near the bug.

• 2201 Javascript-powered per-lemma proof visibility toggling in coqdoc HTML output (fixable)
• 3659 -time should understand multibyte encodings (fixable)
• 2389 coqdoc -g omits "Declare Instance" (see how to make this robust in face of new commands)
• 3334 Typeclasses eauto := bfs has no settable max depth (ask Matthieu, reply wontfix or fix)
• 3026 multiple anomalies in coqchk on CompCert (Pierre L. and Bruno in the same room, check still relevant, see also 2588)
• (SQUASHED: Gregory Malecha) 3936 Pretty-printer gives confusing output for type casts on function applications (fixable, or won't fix)
• 3941 Second character does not appear (fixable with GTK+ skills)
• 4004 [Set Suggest Proof Using] should print suggestions only for objects the user defines, not things defined behind the scenes by the system itself. (fixable via a blacklist or via an extra flag threaded from the seff declaration to the print)
• 4004 request: document behavior of implicit arguments in generalizing binders (Ask Matthieu and document/fix)
• 4045 Incomplete description of "eexact" in the Reference Manual (check if exact and eexact are still different)
• 4084 targets in Makefiles generated by coq_makefile (document the fix and close the bug)
• 3948 Anomaly: unknown constant in Print Assumptions (fixable, PL can help understanding modules)
• 4058 "-schedule-vio-checking" should not be so verbose (unless an option such as -verbose is passed) (fixable)
• 3991 CoqIde does not report error if "Compile Buffer fails" (fixable)

More bugs can be found at the Coq bugzilla. Remember to put the bug in this list if you tackle it, so that others don't tackle the same!