(dirs :standard \ rocq)
