coqtheorem.sty

\ProvidesPackage{coqtheorem}
\RequirePackage{xparse}
\RequirePackage{hyperref}
\RequirePackage{mfirstuc}

\newcommand{\setCoqFilename}[1]{\def\filename{#1}}
\newcommand{\setBaseUrl}[1]{\def\baseurl#1}
\setBaseUrl{}
\setCoqFilename{}
\def\theoremname{}
\def\showname{}
\def\theoremtype{}

\newcommand{\coqlink}[2][]{\href{\baseurl\filename.html\##1}{#2}}

\@ifpackageloaded{paralist}{%
  \newcommand{\coqitem}[1][]{\stepcounter{enumi}\item[{\coqlink[#1]{\labelenumi}}]}
}{%
  \newcommand{\coqitem}[1][]{\stepcounter{enumi}\item[{\coqlink[#1]{\theenumi.}}]}
}%

\newcommand*\ifcounter[1]{%
  \ifcsname c@#1\endcsname
    \expandafter\@firstoftwo
  \else
    \expandafter\@secondoftwo
  \fi
}

\@ifclassloaded{llncs}{
  % If the class is LLNCS:
  \let\theorem\relax
  \let\lemma\relax
  \let\definition\relax
  \let\fact\relax
  \let\corollary\relax

  \newcommand{\genFancyTheoremEnvironment}[1]{%
    \expandafter\newcommand\csname #1AuxCoqautorefname\endcsname{\csname #1autorefname\endcsname}
    \ifcounter{#1}{}{\newcounter{#1}}
    \spnewtheorem{#1Aux}{#1}{\bfseries\theoremtype}{\itshape}
    \spnewtheorem{#1AuxCoq}[#1Aux]{}{\bfseries \coqlink[\theoremname]{\theoremtype}}{{\bfseries\showname}\itshape\label{coq:\theoremname}}
    \NewDocumentEnvironment{#1}{oo}%
    {%
      \def\theoremtype{\capitalisewords{#1}}%
      \IfValueTF{##2}{\def\theoremname{##2}%
        \IfValueT{##1}{\ifx&##1&%
          \else\def\showname{\hspace{-0.6em} (##1)~}\fi}%
        \begin{#1AuxCoq}}
      {\begin{#1Aux}}%
    }%
    {\IfValueTF{##1}{\end{#1AuxCoq}}{\end{#1Aux}}\def\theoremname{}\def\showname{}}}

  \genFancyTheoremEnvironment{theorem}
  \genFancyTheoremEnvironment{lemma}
  \genFancyTheoremEnvironment{definition}
  \genFancyTheoremEnvironment{fact}
  \genFancyTheoremEnvironment{corollary}
}{
  % If not LLNCS

  \RequirePackage{ntheorem}

  \newtheoremstyle{coqtheorem}
  {\linkableTheoremAux{##1}{##2}}
  {\linkableTheoremAux{##1}{##2}[##3]}
  \NewDocumentCommand\linkableTheoremAux{mmou\ignorespaces o}
  {\item[\hskip\labelsep \theorem@headerfont
    \IfValueTF{#5}{\coqlink[#5]{#1\
        #2\IfValueT{#3}{\ifx&#3&%
          \else\ (#3)\fi}{}}}{#1\ #2 \IfValueT{#3}{\ (#3)}{}}
    \theorem@separator]#4\ignorespaces\IfValueT{#5}{\label{coq:#5}}}
}