2016-12-14 environ部 Mizar ダメ出し environ部のディレクティブは2度以上書けるようだが、同じアーティクルが2度以上指定されると、 *810: Directive name repeated これがシンドイ。コピペしかないのに、コピペに不便な仕様。