Notation of cvg can be broken

[IshiguroYoshihiro]

Sometimes notation _ @ _ --> _ is broken after under eq_cvg or under eq_fun.

Here is my example.

From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop.
Require Import signed reals ereal topology normedtype sequences real_interval.
Require Import esum measure lebesgue_measure .

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Example hoge (R : realType) (f : nat -> R) : f x @[x --> \oo] --> 0.
Proof.
under eq_cvg do idtac.
Restart.
under eq_fun do idtac.
Abort.

At first, the goal is

  R : realType
  f : nat -> R
  ============================
  f x @[x --> \oo] --> 0

but the notation is broken by under eq_cvg do idtac :

  R : realType
  f : nat -> R
  ============================
  forall t : set R,
  nbhs
    [set P | (exists2 i : R, [set e | 0 < e] i & ball_ [eta normr] 0 i `<=` P)]
    t -> nbhs (f x @[x --> \oo]) t

there is a similar case for under eq_fun do idtac:

  R : realType
  f : nat -> R
  ============================
  forall t : set R, nbhs 0 t -> nbhs (f x @[x --> \oo]) t