Yeah the main use of it is probably in ELPI which is a higher order structural reasoning and AST transform tool for Coq/Rocq.