Comparing printing of notations and numeral notations

[proux01]

Attempting to merge printing of notations and numeral notations (following a discussion in https://github.com/coq/coq/pull/12163 ), I compared them. Here is a small example illustrating differences.

Notations:

Declare Scope A.
Declare Scope B.
Delimit Scope A with A.
Delimit Scope B with B.
Notation "0" := tt : A.
Notation "1" := tt : B.
Definition f x : unit := x.
Arguments f x%A.
Check f tt.  (* prints f 1%B *)
Open Scope A.
Check tt.  (* prints 1%B *)
Open Scope B.
Notation "1" := true.
Check tt.  (* prints 1 *)

Numeral Notations:

Declare Scope A.
Declare Scope B.
Delimit Scope A with A.
Delimit Scope B with B.
Definition to_unit (v : Numeral.uint) : option unit := Some tt.
Definition of_unit (v : unit) : Numeral.uint := Nat.to_num_uint 0.
Definition of_unit' (v : unit) : Numeral.uint := Nat.to_num_uint 1.
Number Notation unit to_unit of_unit : A.
Number Notation unit to_unit of_unit' : B.
Definition f x : unit := x.
Arguments f x%A.
Check f tt.  (* prints f 0 *)
Open Scope A.
Check tt.  (* prints 0 *)
Open Scope B.
Notation "1" := true.
Check tt.  (* prints 1%B *)

To sum up:

• Open Scope and Arguments change the printing for numeral notations, not for regular ones
• shadowing a notation forces the printing of a delimiter for numeral notations, not for regular ones

Are these differences expected ? If not, which behavior should be favored ?

Coq Version

master

[proux01]

@herbelin you may have an opinion here.

[herbelin]

I feel the numeral notation choice more intuitive (see also #8187).