[ltac] accept constrN, open_constrN and uconstrN as a tactic argument

[gares]

I believe this PR lifts one of the main limitations when it comes to defining tactic syntax without using ocaml (or Ltac2).

[SkySkimmer]

What is this trying to solve and why can't you use ltac2 instead?

[gares]

I will try to use Ltac2, I guess I need a way to call elpi from it.

[gares]

I'm rediscovering the wheel here I guess, but I see I can't call SSR tactics from Ltac2, so the problem is not just Elpi :-/

[gares]

Thanks for the fix, now the code seems more legit.
There is still one bug, the open and u constr variants are interpreted as constr, and I can't really tell why.

[SkySkimmer]

I'm rediscovering the wheel here I guess, but I see I can't call SSR tactics from Ltac2, so the problem is not just Elpi :-/

You should fix that instead of hacking ltac1.

[gares]

Ideally yes, but it is much more work :-(

[SkySkimmer]

IDK if this PR is ever going tobe merged though

[gares]

How hard is to make ARGUMENT/TACTIC extend also edit the Ltac2 grammar?

[SkySkimmer]

It goes against how ltac2 works.

[gares]

Is there a way to have SSR in Ltac2 without rewriting the grammar using Ltac2 notations?

[SkySkimmer]

Some of it may be exposed as ltac2 syntactic classes from ocaml (eg intropatterns)