[==> b1, b2 => b3] does not work (in input)

It works in output.

@ggonthier is that known? is that a new?

It appears so, because it works fine (both ways) in Coq 8.4. Does this affect other n-ary syntax combinators? Did the 8.5 grammar introduce a production for p => E, that would interfere with this rule?

Others look fine, I'll report a bug against Coq then.

reference in Coq's bug tracker: https://coq.inria.fr/bugs/show_bug.cgi?id=4867

I see it with coq 8.12.0 and math-comp 1.12.0.