Karl Palmskog (Jan 05 2023 at 09:07): Karl Palmskog (Jan 05 2023 at 09:07):I've tracked down the source of coqdoc bug 15933, and it's all down to legacy attributes like Program, Polymorphic. Are there any plans to retire these attributes and go all in on #[local], etc.?
My upcoming PR fix is going to be pretty hacky duet to the mere presence of legacy attributes (but hopefully worth it to not have stdlib docs omit a not-insignificant number of sentences).
Théo Zimmermann (Jan 05 2023 at 09:15):There is no plan to remove this syntax at this point (I think this would create too much breakage). But we could start by a project to remove the legacy attributes from the stdlib, and we could document that there is a known issue with coqdoc and legacy attributes.
Karl Palmskog (Jan 05 2023 at 09:24):this kind of stuff is pretty counterintuitive:
Class C := {}.
Succeed Local Program Declare Instance I : C.
Program Declare Local Instance I : C. (* syntax error *)
Local Declare Program Instance I : C. (* syntax error *)
at least with #[program,local] Declare Instance I : C. it's clear that Declare Instance is a unit.
Last updated: Oct 13 2024 at 01:02 UTC