Inconsistency with complex command arguments

[yannl35133]

(Not an elpi user, so my terminology and assumptions may be wrong)

You can define commands which take in multiple arguments, and these (whitespace-separated) arguments can be as simple as references, (brackets-wrapped) terms or as complex as definitions or inductive declarations.

However, whitespace separation of complex arguments doesn't seem consistent: the following works with definitions

From elpi Require Import elpi.
Elpi Command MyCmd.
Elpi Accumulate lp:{{  main [_A,_B] :- coq.say("Hello").  }}.

Elpi MyCmd
  Definition A := I
  Definition B := tt.

but if you replace definitions with inductive declarations it won't (presumably because "Inductive" is not a keyword).

I noticed this issue with coq/coq#20145 where I try to remove the special case of Definition (among others) being a keyword, which breaks this example even with definitions. This is really a simplification of tests/test_arg_HOAS.v#L383-387 which broke the CI in my PR to Coq.

[gares]

Please don't remove the Definition keyword, but rather make Inductive one.

[yannl35133]

Imo the ideal situation would be for elpi's grammar file to promote Definition, Inductive, etc. to keywords, but for Rocq's grammar to have them as identifiers.
There's nothing urgent about my keyword PR and I don't know how to do these changes, so I'll just leave it at that for now

[gares]

Unfortunately the status of keywords is global, so if I make them so in Elpi they also become so in plain Rocq (as soon as elpi is Imported).

FTR they should be keyword to make the grammar less ambiguous and help language servers cope with incomplete text, eg before you type . Intros can literally eat half of what follows.