Xia Li-yao

You can keep this open. Maybe there could be a local workaround or extra doc for this issue in generic-data while it gets resolved upstream.

I wonder how useful the product of monads/applicatives really is. In our paper on bidirectional programming we mainly chose it for simplicity of exposition, but in practice I'd much prefer...

Actually the failure is because we are forcing dune.3.17, probably because of `OPAMIGNORECONSTRAINTS: dune`

Where does the pin on dune.3.17.2 come from? Is it from the rocq docker image?

Fixed by #411

Is any of this not backwards compatible? The error comes from importing `WfExtensionality` which seems to be a mistake. Shouldn't the remaining imports work for existing versions of Coq?

Surprising that this wasn't caught before.

Apparently it's always been `let rec`, so we just never actually got around to extracting `max`

Right, the "attach buffer offsets" task seems to be subsumed by the new ability to convert between the two kinds of offsets at will.