Underscores in hypotheses names causes errors in latex generation

[Casteran]

In coq scripts which contains identifiers with underscores, this character is directly put in the tex file (in particular in the \hypn latex command. For instance the hypothesis H_0 is translated in \begin{hyp}{\hypn{H0}}, without "" being escaped nor pygmentized. At the compilation by latex, the classic error about missing dollars interrupts the compilation.

Example

( underline.v )

Lemma L (H_0 : 1 = 2) (H_1 : 2 = 3) : 1 = 3. Search (?n = S ?n). Fail eapply lt_trans. now rewrite H_1. Qed.

(*

alectryon.py --frontend coq --backend snippets-latex --output-directory . underline.v

pygmentize -S default -f latex > wrapper-underline.pyg

lualatex wrapper-underline.tex

*)

[cpitclaudel]

Fixed in a41483029496774c02d7cfacdfc92d127185e135, thanks!