https://github.com/proof-ninja/rocq/pull/13 で修正中。 ただし、 PR の description に書いてあるとおり、 MLdummy は取り扱いが異なるので別で対応する。
#13 で修正中。
ただし、 PR の description に書いてあるとおり、 MLdummy は取り扱いが異なるので別で対応する。