CoqのModule内定義に関するglobがなんか変な件について.md

mathcomp analysisのtopology.vにおいて，

...
Module PropInFilter : PropInFilterSig.
  Definition t := prop_in_filter_proj.
  ...
End PropInFilter.
Notation prop_of := PropInFilter.t.
...

というコードの，prop_of の行に関するglobファイルの行が次の通り:

abbrev 50509:50515 <> prop_of
R50520:50533 mathcomp.analysis.topology <> t prfax

PropInFilter.t へのレファレンスが　glob上では <> t となっとる！