[Agda] message for `,` without \prime

[mechvel at scico.botik.ru]

Dear Agda team,
I have a program like

   case ((e ≟ₙ e') , (2 ∣ₙ? e'))
   of \
   { (yes _ , yes _) → foo
   ; ...
   }

where  e e' : ℕ.
And Agda 2.6.1.1  reports

-----------------------------------------------------
_B_159 : Dec (deg f _ ≡ deg g _) → Set  [ at /home/...Foo.agda:116,25-26 
]
_163
   : Data.Product.Σ (Dec (deg f _ ≡ deg g _)) _B_159 →
     OverDecComRing.Pol R
     (OfShow.mkShow (λ _ _ ys → 'd' ∷ 'u' ∷ 'm' ∷ 'm' ∷ 'y' ∷ ys))
     dummy-Read "x"  [ at /home/...:116,42-121,27 ]

———— Errors —————————————————————————————
Failed to solve the following constraints:
   Dec
   ((Algebra.Monoid.semigroup ℕp.*-1-monoid OfSemigroup.∣ 2)
    (deg g _))
     =< _B_159 (deg f _ ≟ₙ deg g _)
-----------------------------------------------------

And it is type-checked if  `,' is changed to ",′"
in the head line of `case`.

I do not know of whether the report can be made more helpful.
I just show this example for any occasion.

Regards,

------
Sergei