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:
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:
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,
ProofGeneral-devel mailing list

Reply via email to