There is a coq flag called Silent
. But I can't seem to work out what it does. I have a .v file that prints something but setting Silent
doesn't seem to change anything with coqc
For example:
$ echo "Require Import Basics. Set Silent. Print Eq." > test.v
$ coqc test.v
Inductive comparison : Set :=
Eq : comparison | Lt : comparison | Gt : comparison
What exactly was it supposed to do?
This line of code shows that -batch
implies -quiet
so there are good chances that this flag has no effect when used with coqc
and is only useful to avoid printing goals when using coqtop
.
Thanks!
Last updated: Oct 13 2024 at 01:02 UTC