The Coq development builds binary compilers that generate code using some implementation strategy. The parameters (modulus, hardware multiplication input bitwidth, etc.) are are specified on the command line of the compiler. The generated C code is written to standard output.