The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

My guess is that it's a historical accident.  I suspect `coqc` started out as a thin wrapper for `coqtop -compile` (though I am by no means confident about this), and inherited the default options.

On Sat, Oct 26, 2019 at 1:27 PM Ian Zimmerman <itz AT very.loosely.org> wrote:

On 2019-10-26 02:30, Jason Gross wrote:

> I believe .coqrc is intended for local commands that you might want for
> interactive use, but not globally.  e.g., you might have a different
> preferred printing width (Set Printing Width) or depth (Set Printing
> Depth).

This sounds sensible, but why does coqc also obey the commands in this
file, in such case?

--
Please don't Cc: me privately on mailing lists and Usenet,
if you also post the followup to the list or newsgroup.
To reply privately _only_ on Usenet and on broken lists
which rewrite From, fetch the TXT record for no-use.mooo.com.