building pdf fails because of comments

[Andrzej Giniewicz]

Hi,

I was following the project for quite a while, you are doing quite
impressive work here! 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), but building pdf fails - as I found
out because of using % - i.e. if the part is of form:

(** %
A
% comment
B.
% *)

it typesets A as it should, then "comment B" as-is without parsing,
and then start typesetting from "*) ..." as TeX again, making it just
fail. Removing comments helped and the document built. At end of this
mail I will attach where are the offending % I found. I'd provide
patch, but I didn't found a way to output % into .tex file. The %%%%
which I hoped would work (end processing, output % by double % to
escape it, start processing again) outputs "\%" actually instead of
single %.

Cheers,
Andrzej.

catches.v:105
     %

catches.v:189
% XXX We don't allow undo catches in the repo yet
% $\seq{c} \seq{d} \seq{d}^$ is a repo if $\seq{c} \seq{d}$ is a repo and
% all of $\names{\seq{d}}$ are positive.

catches.v:202
% XXX this is if we don't have a special inverse comflictor constructor:
% \conflictor{Es}{Z}{Ps:p}^
% = \conflictor{Es^}{\mkset{(Es Qs q : q^) \mid (Qs : q) \in Z}}{Es Ps p:p^}

catch_patch_universe.v:109
$\pair{\conflictor{\seq{r} \seq{s}}{W}{x}}%

catch_patch_universe.v:111
\pair{\conflictor{\seq{r} \seq{t'}}{\seq{s'}Y}{\seq{s'}z}}%

catch_patch_universe.v:115
$\pair{\conflictor{\seq{r} \seq{t'}}{(\seq{s'}Y)}{(\seq{s'}z)}}%

catch_patch_universe.v:120
\pair{\conflictor{\seq{r} \seq{t'}}{(\seq{s'}Y)}{(\seq{s'}z)}}%

catch_patch_universe.v:123
\pair{\conflictor{\seq{r} \seq{s}}{\seq{t}(\seq{t}^W)}{\seq{t}(\seq{t}^x)}}%

catch_patch_universe.v:133
$\pair{\conflictor{\seq{r} \seq{t'}}{(\seq{s'}Y)}{(\seq{s'}z)}}%

catch_patch_universe.v:136
\pair{\conflictor{\seq{r} \seq{s}}{W}{x}}%

contexted_patches.v:226
% XXX Proove that this is symmetric