aboutsummaryrefslogtreecommitdiff
path: root/lib/errors.mli
diff options
context:
space:
mode:
authorEnrico Tassi2015-05-28 19:00:07 +0200
committerEnrico Tassi2015-05-29 15:44:47 +0200
commitf63c0cdd3c7da642e505569e83199784bbfdc367 (patch)
tree6556a9e2f016d56cb70849c5ef75a9a545f95527 /lib/errors.mli
parentc47916933025a4853ed0b397d7476b844bb894a4 (diff)
make Unset Silent work in coqc
Trying to untangle the flags: coqc -verbose coqtop -compile-verbose are used just to print the commands run; -quiet, -silent, Set Silent, Unset Silent control Flags.verbose flag. Flags.verbose controls many prints that are expected to be made in interactive mode. E.g. "Proof" or "tac" prints goals if such flag is true. To flip it, one can "Set/Unset Silent" in both coqtop and coqc mode. It is still messy, but the confusion between -verbose and Flags.verbose has gone (I must have identified the two things with my initial STM patch)
Diffstat (limited to 'lib/errors.mli')
0 files changed, 0 insertions, 0 deletions