The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements.
Introduce a global test_verbosity and a verbosity that handle verbosity in output of tests and of normal statements respectively. As a consequence, the standard compilation process should now be silent: if tests pass, there is no output.
Introduce a global
test_verbosityand averbositythat handle verbosity in output of tests and of normal statements respectively. As a consequence, the standard compilation process should now be silent: if tests pass, there is no output.