The Coq mailing list

[Ian Zimmerman <itz AT very.loosely.org>]

On 2019-10-12 22:58, Gaëtan Gilbert wrote:

> > So ... -init-file is getting passed correctly, but it has no effect
> > because it is accompanied by -q.  Why does coq_makefile pass -q to
> > coqc, and how can I change this behavior?

> make COQFLAGS=

Thanks, I didn't use this literally but it showed me the way.

But now, how to make this work in coqide?  Nothing I tried so far worked
- usually coqide refuses to even start, saying "coqidetop stopped badly"
or something like that.  If I don't do anything it starts OK but it
won't parse any file that contains ssreflect notations.

This is the same with coqide 8.9 (Gtk 2 based) and 8.10 (Gtk 3 based).

Everything works if I put those imports in my _global_ ~/.coqrc but I
don't want to do that - among other reasons because then at least one
opam package fails to build, not isolating itself from the local
configuration.

-- 
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.