aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/coq/multiple/README
blob: 1450115bd381c2611a2f732983bf4dd89c11da46 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
Multiple files in PG 3.5 / Coq 8.0

The option "auto-compile-vos" has been fixed up somewhat for this
release.  Please report any problems to David Aspinall (da@inf.ed.ac.uk)

Strategy is:

- When scripting is turned *off* in a buffer, you will be asked if you
want to save it, and then either M-x compile is run (if PG sees a
Makefile in the same directory), or coqc on just the buffer is run.
(You can customize this behaviour by setting compile-command and/or
coq-compile-file-command).
[ Desirable improvement: query user to save any dependent files ]