Hugo wants to discuss focusing our collective efforts on tactics (Ali)
We have a lot of tactics, this is confusing for users
Adding features to tactics is difficult, no consensus on simplicity vs usability
disparity between coq, ssreflect, commonly defined tactics etc.
Notes
PR 11327: needs more thought, can we avoid entangling parsing/scope interpretation and typing while implementing this feature.
Schemes: easy to fix the induction tactic lookup thing. A hook for declaring things after the definition of an inductive/constant that is plugin or even user extensible would be enough to handle.
Discussion about using namespaces and allowing the nat_rect -> nat.rect change Hugo is proposing. Should be fine if it does not go in conflict with the current namespace CEP.