Coq prints {| |} but cannot parse it

[gares]

If you define an empty record Coq prints its constructor a {| |} but then it cannot parse it back since it wants the name of a field.
IMO the notation system should check the number of fields in order to decide weather to use the notation or not.

CC @coq/extensible-syntax-maintainers

[herbelin]

Hi @gares, can you give an example where an empty record is printed as {| |}? In any case, if it is so, why not to relax instead the expectation of at least one field, so that, e.g., if there is a type constraint, the notation {| |} is accepted?

[gares]

That would be a better behaviour indeed

[gares]

It took me a while, it needs to have parameters:

Module Bug. Record foo (A : Type) := {}. End Bug.
Definition bug := Bug.Build_foo nat.
Print bug.
(*
bug = {| |}
     : Bug.foo nat
*)

[gares]

I guess there is already a test to see if the record is empty (and print the constructor name instead) but the test does not consider that some arguments of the constructor are not fields.

[gares]

In addition to that, if the record has parameters, they are hidden by the {| ... |} even if Set Printing Implicits is on