The Coq mailing list

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

I am trying to enhance my minimal knowledge of coq in the following
context:

- classical logic
- ssreflect tactic language
- unicode symbols

This means that every one of my .v files needs the following boilerplate
at the beginning:

From mathcomp Require Import ssreflect ssrfun ssrbool.
Require Import FunctionalExtensionality.
Require Import ClassicalEpsilon.
Require Import PropExtensionality.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require Import Utf8.

So far the only way I've thought of to avoid in fact typing all this is
to use the "initfile" or "rcfile".  So I added this to my _CoqProject:

-arg -init-file
-arg ,coqinit

where the contents of ,coqinit are as above.

And I see that after running coq_makefile, make VERBOSE=1 does something
like:

 matica!41 ssreflect-playground$ make VERBOSE=1
"coqdep" -dyndep var -f _CoqProject   > ".coqdeps.d" || ( RV=$?; rm -f 
".coqdeps.d"; exit $RV )
make --no-print-directory -f "Makefile" pre-all
if [ "8.9.1" != "8.9.1" ]; then\
  echo "W: This Makefile was generated by Coq 8.9.1";\
  echo "W: while the current Coq version is 8.9.1";\
fi
make --no-print-directory -f "Makefile" real-all
"coqc"   -q  -init-file ,coqinit  -R . Top Group_abstract.v 
File "./Group_abstract.v", line 3, characters 42-45:
Error: Syntax Error: Lexer: Undefined token

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?

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