As was highlighted in #81, there is no documentation for some preamble homs such as coq-preamble. The latter hom is crucial for generating Coq files that compile using the locally nameless backend, and should ideally be highlighted in the documentation for that backend.
In the manual source (top2.mng), we have the following commented out, which should ideally be rewritten with the above in mind:
% Ott also permits embed blocks with \mykw{tex-preamble},
% \mykw{hol-preamble}, or \mykw{isa-preamble} homs.
% The contents of these appear (respectively) in the \LaTeX{} preamble,
% just before the HOL \texttt{val \_ = new\_theory}, or between the Isabelle
% \texttt{imports Main Multiset} and \texttt{begin}.
% Any definitions of \LaTeX{} commands must appear in such a
% \mykw{tex-preamble} section.
As was highlighted in #81, there is no documentation for some preamble homs such as
coq-preamble. The latter hom is crucial for generating Coq files that compile using the locally nameless backend, and should ideally be highlighted in the documentation for that backend.In the manual source (
top2.mng), we have the following commented out, which should ideally be rewritten with the above in mind: