CoqdocJS does not understand "Next Obligation"
Looks like CoqdocJS doesn't understand that the new Next Obligation
syntax also starts a proof that should be hidden by default.
Looks like CoqdocJS doesn't understand that the new Next Obligation
syntax also starts a proof that should be hidden by default.