HB breaks the parsing of commas (tuples, "in" clauses, etc)

[silene]

From HB Require Import structures.

Lemma foo (v1: plus 1 2 = 0) : False.
Proof.
unfold plus in v1, v1.
(* Syntax error: [in_clause] expected after 'in' (in [clause]). *)
Check (v1, v1).
(* Syntax error: [term level 200] expected after '(' (in [term]). *)

A space is now needed before commas, e.g., unfold plus in v1 , v1.

[gares]

@CohenCyril I'm not very good with notations, and since this code is copy pasted from an old code of mine the problem could be here:

https://github.com/math-comp/hierarchy-builder/blob/9d256b8ec2d8de15975aa8de94cd1336cb41f070/HB/structures.v#L1212C1-L1220C14

@silene if you rename v1 into w1, does it work? Maybe the problem is that v1, is now a keyword.

[gares]

I don't see any other possible causes, but admit all my ignorance on the subject...

[silene]

Indeed, this is the likely culprit.

Print Grammar constr.
(*
| "0" LEFTA
  [ "[find"; "v1,"; "..,"; term LEVEL "200"; "|"; term LEVEL "200"; "∼"; term LEVEL "200"; "]"; NEXT
*)

I guess you can just remove this notation since it obviously has never been used.

[gares]

I wonder what the RHS of the notation looks like internally...
Anyway I opened a PR