Hi Hendrik, > your first email got through and thanks for you positive > feedback!
Thanks or the quick reply! > I have the impression that you have not read any documentation > about the quick compilation feature. The CHANGES file is > unfortunately not the place to describe a complex feature > completely, but it contains a pointer: "See the option > `coq-compile-quick' or the subsection "11.3.3 Quick compilation > and .vio Files" in the Coq reference manual." May I ask that you > follow one of these links? I believe all your questions are > answered there and you will also find the documentation about the > feature that you are requesting! Unfortunately, the CHANGES file does not contain any links (as in literal hyperlinks) to the right sections, and if I look up section 11.3.3 of the reference manual myself, this is where I end up: <https://coq.inria.fr/refman/Reference-Manual013.html#sec515> That's... probably not the section you meant ;) I have to admit I did not consult that document before writing the mail, because many of my questions are PG-specific and I did not expect any help about that in the Coq reference manual. I should of course still have done the lookup, in which case however I'd have been stuck at the above document. I only just now realized you are talking about the *ProofGeneral* reference manual, a document of which I didn't even know it existed: <https://proofgeneral.github.io/doc/userman/ProofGeneral_12/#Coq-Proof-General> Maybe the text in the CHANGES file could be improved to clarify which reference manual it is talking about. After all, when referring to a Coq feature, a reference to the Coq reference manual (the one linked to in my first paragraph) is not entirely unexpected -- but clearly, that's not what is meant here. I may come back later with more questions, once I read the docs ;) Kind regards, Ralf _______________________________________________ ProofGeneral-devel mailing list ProofGeneralfirstname.lastname@example.org http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel