Open david-christiansen opened 6 days ago
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.
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.