Extended reals notations shows up unexpectedly

[CohenCyril]

From mathcomp Require Import all_ssreflect ssralg ereal.

Open Scope ring_scope.

Goal forall (R : nmodType) (x : R), x + x = x.

is displayed wrongly:

  ============================
  forall (R : nmodType) (x : R), (x + x)%E = x

(everything is fine if ereal is not imported)

[proux01]

Likely

analysis/reals/constructive_ereal.v

Lines 480 to 481 in e9483b0

	Notation "x + y" := (GRing.add (x%dE : \bar^d _) y%dE) : ereal_dual_scope.
	Notation "x + y" := (GRing.add x%E y%E) : ereal_scope.

that is not precise enough

[CohenCyril]

Likely

analysis/reals/constructive_ereal.v

Lines 480 to 481 in e9483b0

Notation "x + y" := (GRing.add (x%dE : \bar^d _) y%dE) : ereal_dual_scope.
Notation "x + y" := (GRing.add x%E y%E) : ereal_scope.
that is not precise enough

It looks like the only possible origin, but it still does not explain why the ereal_scope is triggered in the first place