Documentation nit: Use `(**` rather than `(*` if you want the coqdoc-generated documentation to pick this up.