Small fix to handling of comments within proofs (BofL)

[jeromesimeon]

Fixes problems when handling (* when within a proof and at beginning of line.

[xavierleroy]

Thanks for the suggestion, but off the top of my head I don't visualize the problem that is being solved here and how it is solved. Would you have an example or two?

[jeromesimeon]

I should probably have explained better in the pull request (or simply have opened an issue?). Here is a small example in Coq, with the output (copied-pasted from HTML) before and after the fix:

In Coq:

    Lemma In_app_comm {A} (v:A) (l1 l2:list A) :
      In v (l1++l2) -> In v (l2++l1).
    Proof.
      apply Permutation_in. (* from in to permutations *)
      (* commuting app preserves permutation *)
      apply Permutation_app_comm.
    Qed. 

In HTML, before the fix:

    Lemma In_app_comm {A} (v:A) (l1 l2:list A) :
      In v (l1++l2) -> In v (l2++l1).
Proof.
      apply Permutation_in. (* from in to permutations *)
 commuting app preserves permutation *)      apply Permutation_app_comm.
    Qed.

The fix is for handling opening comments at the beginning of lines within proofs, so it would look as follows in HTML after the fix:

    Lemma In_app_comm {A} (v:A) (l1 l2:list A) :
      In v (l1++l2) -> In v (l2++l1).
Proof.
      apply Permutation_in. (* from in to permutations *)
      (* commuting app preserves permutation *)
      apply Permutation_app_comm.
    Qed.

I'm not sure how to reproduce the colors in here, but the comments inside the proofs are preserved, and show with a nice green color.

[xavierleroy]

Thanks for the explanation and example, very useful. Merging!

[jeromesimeon]

Great! Thanks!