diff options
| -rw-r--r-- | tools/coqdoc/coqdoc.sty | 5 | ||||
| -rw-r--r-- | tools/coqdoc/index.ml | 2 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 2 |
3 files changed, 3 insertions, 6 deletions
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index 4314d07d6f..9de9a38ff9 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -83,7 +83,7 @@ \newcommand{\coqdocnotation}[1]{\coqdockw{#1}} \newcommand{\coqdocsection}[1]{\coqdoccst{#1}} \newcommand{\coqdocaxiom}[1]{\coqdocax{#1}} -\newcommand{\coqdocmoduleid}[1]{\coqdocmod{#1}} +\newcommand{\coqdocmodule}[1]{\coqdocmod{#1}} % Environment encompassing code fragments % !!! CAUTION: This environment may have empty contents @@ -107,9 +107,6 @@ % Empty lines (in code only) \newcommand{\coqdocemptyline}{\vskip 0.4em plus 0.1em minus 0.1em} -% macro for typesetting the title of a module implementation -\newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{} -} \usepackage{ifpdf} \ifpdf \RequirePackage{hyperref} diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index d9f5d9e1ef..dbb0c1d6be 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -213,7 +213,7 @@ let type_name = function | Library -> let ln = !lib_name in if ln <> "" then String.lowercase ln else "library" - | Module -> "moduleid" + | Module -> "module" | Definition -> "definition" | Inductive -> "inductive" | Constructor -> "constructor" diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 76c20fb02a..53fee9875f 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -285,7 +285,7 @@ module Latex = struct printf "\\coqdocindent{%2.2fem}\n" space let module_ref m s = - printf "\\moduleid{%s}{%s}" m (escaped s) + printf "\\coqdocmodule{%s}{%s}" m (escaped s) let ident_ref m fid typ s = let id = if fid <> "" then (m ^ "." ^ fid) else m in |