ssreflect を使っているとき，proofgeneral のデフォルトのままだと（といっても何が本当にデフォルトなのか把握できていませんが，少なくともそんなにいじってないはずの手元の環境では）インデントがあんまりうまくいってない感じが強いので何とかできない…

Coq の証明を書くときに，ただ tactics を一列に並べて書くと，まったく読めなかったり Coq のバージョンが上がって証明が通らなくなったときにどこでこけてるのかわからなくなったりして不都合なので，証明の構造を proof script のテキスト上にも反映させ…