From b62f4058b45f8fab24885b030b85ed1ca328445c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 4 Dec 2010 10:34:16 +0000
Subject: 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
---
 tools/coqdoc/coqdoc.sty | 5 +----
 tools/coqdoc/index.ml   | 2 +-
 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
-- 
cgit v1.2.3