The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

I was surprised to the result of this code after deactivating the
display of notations:

>>>
Definition plus_ (m n: nat) := m.
Definition lt_ (m n: nat) := true.

Notation "n + m" := (plus_ m n).
Notation "m < n" := (lt_ m n).

Check (forall m n, (forall o, true = (m< ( n+o ) ))).
Check (forall n, (forall o, 0 = ( n+o ) )).
<<<

in the first case, n+o is interpreted as the coq defined "plus", but in
the second case it is interpreted as "plus_".

I expected "( x )" to put 'x' at level 200, so that would force the
interpretation of "x < y" to be the same in both cases.

Is there some explanation of this thing? Has this behaviour been
changed along coq versions?

Thanks
Cédric.