- add hole command for sanity check (note: hole commands only work when an expression is expected, not when a command is expected, which is unfortunate)
- print the type of the unused arguments
- print whether an unused argument is a duplicate
- better check to filter automatically generated declarations
- do not print arguments of type `parse _`
- The binding brackets from `tactic.where` are moved to `meta.expr`. The definition is changed so that strict implicit arguments are printed as `{{ ... }}`

Fun fact: I had to remove an unused argument from `decidable_chain'` for my function to work.