coq-mod-reduce This plugin provides a way to bundle a set of terms together and supply them all to the [cbv] reduction mechanism. Example See the test-suite directory for several examples.