ltac: API for simple tactics

[gares]

• calling Ltac returns a diagnostic
• APIs for calling tactics that do not change the proof context, and hence return goals in place of sealed-goals
• requires Elpi 3.6

TODO:

• refactor in_coq_context to generate hyps, use that for the TODO in collect-simple-goals