Synterp code of creating notations unnecessarily uses notation's body

[trilis]

Refactoring request

It seems strange to me that to call synterp part of creating notations (Metasyntax.add_notation_syntax), I need to pass notation body as the part of notation_declaration structure (ntn_decl_interp field — it even has interp in its name :) ). Inspecting the code, I came to conclusion that the only place where the body is actually used is changing the term in case of infix notations. I suppose that infix flag can be remembered for interp code, and interp code can change the term however it likes.

Additional context

The context here is that I want to add to coq-elpi (cc @gares) builtins for creating notations (it currently has API for abbreviations, but we need full-blown notations with custom scopes, levels, etc). For our elpi fork, we just use placeholder Constrexpr.CHole (None) in synterp code and then call add_notation_syntax again in interp code, this time with the actual body. It works (as we don't use infix notations), but I want a prettier solution before submitting PR to public elpi.

[SkySkimmer]

I suppose that infix flag can be remembered for interp code, and interp code can change the term however it likes.

Sounds reasonable. Do you intend to try to make this change or are you asking for someone else to do it?

[trilis]

Sure, I can try in the next couple of days. I will need some help with adapting external plugins and libs to this change though, as I have no idea how adapting process works in the coq community