Open
Description
There should be dedicated indices for options, commands, declarations, tactics, inductive types, constructors, and syntax organized by atoms found in their grammar, in addition to the current comprehensive index.
{{ message }}
No one assigned
No type
No projects
No milestone
None yet
No branches or pull requests