Notations "at level 200" are actually put in binder_constr, subentry of level 10

[SkySkimmer]

rocq/vernac/egramrocq.ml

Line 325 in c4fa328

if level = 200 then Constr.binder_constr, None

binder_constr was at level 200 before #18014

The current situation seems nonsensical but I'm not sure how best to resolve it.

BTW using a subentry means SELF only produces the subentry, eg

Notation "x 'foo' y" := (x -> y) (at level 200).

Check nat foo nat. (* does not parse *)

why is binder_constr not inlined in the appropriate level?

[SkySkimmer]

cc @proux01

[SkySkimmer]

(and the pattern side of the notation is still going in level 200)

[SkySkimmer]

experiment at #21671