building pdf fails because of comments

[Ian Lynagh]

Hi Andrzej,

On Wed, Dec 08, 2010 at 03:47:39PM +0100, Andrzej Giniewicz wrote:
> 
> I was following the project for quite a while, you are doing quite
> impressive work here!

Thanks!

> When I noticed, that camp switched to coq 8.3
> (which comes with my distro) I decided to give it a try. The build
> "make coq" goes fine (after update to latest 8.3 from svn, though as I
> started already I did that too),

Right, I ran into a couple of show-stopper coq bugs in the last few
days, so you really do need the latest patches from the branch.

Incidentally, what I'm currently working on is a proof that catches
satisfy the patchlike axioms.

> but building pdf fails

Sorry about that; I've been focussing on the proof lately, so not
building the PDF.

(and as a result, the PDF is probably a bit out of sync with the proofs.
And generally lacking in text for that matter).

> but I didn't found a way to output % into .tex file.

The trick is to give up, and use # instead  :-)

    % We can't use % as a comment character in files that go through coqdoc,
    % as it uses that as the latex escape character. Sigh. So we use #
    % instead.
    \catcode`\#14

I've pushed a patch to fix this up, and also correct a few include
paths.


Thanks
Ian