Better fix to bug #2183 ("moduleid" internal name got exposed to users

in coqdoc index files).

Bug #2183 was fixed by changing "module" into "moduleid" in Index.type_name
instead of changing "moduleid" into "module". But "moduleid" is used
for building the html indexes what led to not very nice output (one
would expect to see "module" in the index).

Apparently, the reason "moduleid" was used instead of "module" as
internal name for rendering module in the TeX output of coqdoc was
that there were already an old \coqdocmodule historically introduced
by Jean-Christophe to format libraries.  But this \coqdocmodule seems
to have been replaced by a \coqlibrary by Matthieu in r11065. So I
conclude that Jean-Christophe's use of \coqdocmodule in coqdoc.sty is
definitively obsolete, that the \coqmodule LaTeX command is free for
other uses and that \coqdocmoduleid has no reason not to be called
\coqdocmodule, and consequently, module has no reason to be some
moduleid in Index.type_name.

Moreover, it remained a \moduleid in Output.module_ref ? Shouldn't it
be \coqdocmoduleid (or actually \coqdocmodule, since the id suffix is
apparently no longer needed).

Hoping I'm not doing something wrong.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13675 85f007b7-540e-0410-9357-904b9bb8a0f7

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