Avoid generated names for html pages of the reference manual (bug #4742).

33 files changed, 33 insertions, 0 deletions

diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex
index eee41a679..856a823de 100644
--- a/doc/refman/AddRefMan-pre.tex
+++ b/doc/refman/AddRefMan-pre.tex
@@ -4,6 +4,7 @@
 \setheaders{Presentation of the Addendum}
 %END LATEX
 \chapter*{Presentation of the Addendum}
+%HEVEA\cutname{addendum.html}
 
 Here you will find several pieces of additional documentation for the
 \Coq\ Reference Manual. Each of this chapters is concentrated on a
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 1609e4a04..30039d489 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -1,4 +1,5 @@
 \achapter{Asynchronous and Parallel Proof Processing}
+%HEVEA\cutname{async-proofs.html}
 \aauthor{Enrico Tassi}
 
 \label{pralitp}
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex
index 275e1c2d5..8961b0096 100644
--- a/doc/refman/CanonicalStructures.tex
+++ b/doc/refman/CanonicalStructures.tex
@@ -1,4 +1,5 @@
 \achapter{Canonical Structures}
+%HEVEA\cutname{canonical-structures.html}
 \aauthor{Assia Mahboubi and Enrico Tassi}
 
 \label{CS-full}
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index a95d8114f..7ad895f9d 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -1,4 +1,5 @@
 \achapter{Extended pattern-matching}
+%HEVEA\cutname{cases.html}
 %BEGIN LATEX
 \defaultheaders
 %END LATEX
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 7e07868a3..22c75b4fc 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -6,6 +6,7 @@
 \newcommand\tele[1]{\overrightarrow{#1}}
 
 \achapter{\protect{Type Classes}}
+%HEVEA\cutname{type-classes.html}
 \aauthor{Matthieu Sozeau}
 \label{typeclasses}
 
diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex
index 16006a6ad..ec46e1eb5 100644
--- a/doc/refman/Coercion.tex
+++ b/doc/refman/Coercion.tex
@@ -1,4 +1,5 @@
 \achapter{Implicit Coercions}
+%HEVEA\cutname{coercions.html}
 \aauthor{Amokrane Saïbi}
 
 \label{Coercions-full}
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 499239b6f..83e866e9f 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -1,4 +1,5 @@
 \achapter{Extraction of programs in Objective Caml and Haskell}
+%HEVEA\cutname{extraction.html}
 \label{Extraction}
 \aauthor{Jean-Christophe Filliâtre and Pierre Letouzey}
 \index{Extraction}
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex
index 4daf98f87..2617142f5 100644
--- a/doc/refman/Micromega.tex
+++ b/doc/refman/Micromega.tex
@@ -1,4 +1,5 @@
 \achapter{Micromega: tactics for solving arithmetic goals over ordered rings}
+%HEVEA\cutname{micromega.html}
 \aauthor{Frédéric Besson and Evgeny Makarov}
 \newtheorem{theorem}{Theorem}
 
diff --git a/doc/refman/Misc.tex b/doc/refman/Misc.tex
index e953d2f70..ab00fbfe3 100644
--- a/doc/refman/Misc.tex
+++ b/doc/refman/Misc.tex
@@ -1,4 +1,5 @@
 \achapter{\protect{Miscellaneous extensions}}
+%HEVEA\cutname{miscellaneous.html}
 
 \asection{Program derivation}
 
diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex
index 70e36a5ee..1401af10f 100644
--- a/doc/refman/Nsatz.tex
+++ b/doc/refman/Nsatz.tex
@@ -1,4 +1,5 @@
 \achapter{Nsatz: tactics for proving equalities in integral domains}
+%HEVEA\cutname{nsatz.html}
 \aauthor{Loïc Pottier}
 
 The tactic \texttt{nsatz} proves goals of the form
diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex
index 1610305e7..8025fbe29 100644
--- a/doc/refman/Omega.tex
+++ b/doc/refman/Omega.tex
@@ -1,5 +1,6 @@
 \achapter{Omega: a solver of quantifier-free problems in
 Presburger Arithmetic}
+%HEVEA\cutname{omega.html}
 \aauthor{Pierre Crégut}
 \label{OmegaChapter}
 
diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
index 77d592834..d9b8b8c52 100644
--- a/doc/refman/Polynom.tex
+++ b/doc/refman/Polynom.tex
@@ -1,4 +1,5 @@
 \achapter{The \texttt{ring} and \texttt{field} tactic families}
+%HEVEA\cutname{ring.html}
 \aauthor{Bruno Barras, Benjamin Gr\'egoire, Assia
   Mahboubi, Laurent Th\'ery\footnote{based on previous work from
   Patrick Loiseleur and Samuel Boutin}}
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index f60908da6..1e204dc83 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -1,4 +1,5 @@
 \achapter{\Program{}}
+%HEVEA\cutname{program.html}
 \label{Program}
 \aauthor{Matthieu Sozeau}
 \index{Program}
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index ad795d406..0dbfe05d4 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -2,6 +2,7 @@
 \label{Cic}
 \index{Cic@\textsc{CIC}}
 \index{Calculus of Inductive Constructions}}
+%HEVEA\cutname{cic.html}
 
 The underlying formal language of {\Coq} is a {\em Calculus of
 Inductive Constructions} (\CIC) whose inference rules are presented in
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 45230fb6e..9790111f1 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -2,6 +2,7 @@
 \ttindex{coqtop}
 \ttindex{coqc}
 \ttindex{coqchk}}
+%HEVEA\cutname{commands.html}
 
 There are three \Coq~commands: 
 \begin{itemize}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 7af4e9313..b27a4dc94 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1,4 +1,5 @@
 \chapter[Extensions of \Gallina{}]{Extensions of \Gallina{}\label{Gallina-extension}\index{Gallina}}
+%HEVEA\cutname{gallina-ext.html}
 
 {\gallina} is the kernel language of {\Coq}. We describe here extensions of
 the Gallina's syntax.
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index ef12fe416..df0cd2b82 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1,5 +1,6 @@
 \chapter{The \gallina{} specification language
 \label{Gallina}\index{Gallina}}
+%HEVEA\cutname{gallina.html}
 \label{BNF-syntax} % Used referred to as a chapter label
 
 This chapter describes \gallina, the specification language of {\Coq}.
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index c6fbd1c53..75f3d18de 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -1,5 +1,6 @@
 \chapter[\Coq{} Integrated Development Environment]{\Coq{} Integrated Development Environment\label{Addoc-coqide}
 \ttindex{coqide}}
+%HEVEA\cutname{coqide.html}
 
 The \Coq{} Integrated Development Environment is a graphical tool, to
 be used as a user-friendly replacement to \texttt{coqtop}. Its main
diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex
index 2b9e4e605..f802a3595 100644
--- a/doc/refman/RefMan-int.tex
+++ b/doc/refman/RefMan-int.tex
@@ -2,6 +2,7 @@
 \setheaders{Introduction}
 %END LATEX
 \chapter*{Introduction}
+%HEVEA\cutname{introduction.html}
 
 This document is the Reference Manual of version \coqversion{} of the \Coq\ 
 proof assistant. A companion volume, the \Coq\ Tutorial, is provided
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 4ebb484e7..c8e844302 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -1,4 +1,5 @@
 \chapter[The {\Coq} library]{The {\Coq} library\index{Theories}\label{Theories}}
+%HEVEA\cutname{stdlib.html}
 
 The \Coq\ library is structured into two parts:
 
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 3ce1d4ecd..c8e2ae2dd 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1,4 +1,5 @@
 \chapter[The tactic language]{The tactic language\label{TacticLanguage}}
+%HEVEA\cutname{ltac.html}
 
 %\geometry{a4paper,body={5in,8in}}
 
diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex
index 2019a529f..7c672cf42 100644
--- a/doc/refman/RefMan-modr.tex
+++ b/doc/refman/RefMan-modr.tex
@@ -1,4 +1,5 @@
 \chapter[The Module System]{The Module System\label{chapter:Modules}}
+%HEVEA\cutname{modules.html}
 
 The module system extends the Calculus of Inductive Constructions
 providing a convenient way to structure large developments as well as
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 8f43ebcfb..60cd8b73a 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -1,5 +1,6 @@
 \chapter[Vernacular commands]{Vernacular commands\label{Vernacular-commands}
 \label{Other-commands}}
+%HEVEA\cutname{vernacular.html}
 
 \section{Displaying}
 
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 0c2a18eb2..991c9745e 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -2,6 +2,7 @@
 \setheaders{Credits}
 %END LATEX
 \chapter*{Credits}
+%HEVEA\cutname{credits.html}
 %\addcontentsline{toc}{section}{Credits}
 
 \Coq{}~ is a proof assistant for higher-order logic, allowing the
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index eb59ca584..8f659ded3 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -1,5 +1,6 @@
 \chapter[Proof handling]{Proof handling\index{Proof editing}
 \label{Proof-handling}}
+%HEVEA\cutname{proof-handling.html}
 
 In \Coq's proof editing mode all top-level commands documented in 
 Chapter~\ref{Vernacular-commands} remain available
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index 23a1c9b02..956f30851 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -1,4 +1,5 @@
 \chapter{Proof schemes}
+%HEVEA\cutname{schemes.html}
 
 \section{Generation of induction principles with {\tt Scheme}}
 \label{Scheme}
diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex
index db794e5a6..be199e0b2 100644
--- a/doc/refman/RefMan-ssr.tex
+++ b/doc/refman/RefMan-ssr.tex
@@ -1,4 +1,5 @@
 \achapter{The SSReflect proof language}
+%HEVEA\cutname{ssreflect.html}
 \aauthor{Georges Gonthier, Assia Mahboubi, Enrico Tassi}
 
 \newcommand{\ssr}{{\sc SSReflect}}
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index d8a353300..eecb5ac7c 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -1,4 +1,5 @@
 \chapter[Syntax extensions and interpretation scopes]{Syntax extensions and interpretation scopes\label{Addoc-syntax}}
+%HEVEA\cutname{syntax-extensions.html}
 
 In this chapter, we introduce advanced commands to modify the way
 {\Coq} parses and prints objects, i.e. the translations between the
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 8fbcfdf30..a2d45046b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3,6 +3,7 @@
 \chapter{Tactics
 \index{Tactics}
 \label{Tactics}}
+%HEVEA\cutname{tactics.html}
 
 A deduction rule is a link between some (unique) formula, that we call
 the {\em conclusion} and (several) formulas that we call the {\em
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index cb8f916f1..7cdb1a527 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -1,4 +1,5 @@
 \chapter[Detailed examples of tactics]{Detailed examples of tactics\label{Tactics-examples}}
+%HEVEA\cutname{tactic-examples.html}
 
 This chapter presents detailed examples of certain tactics, to
 illustrate their behavior.
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index f6371f8e5..ed41e3216 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -1,4 +1,5 @@
 \chapter[Utilities]{Utilities\label{Utilities}}
+%HEVEA\cutname{tools.html}
 
 The distribution provides utilities to simplify some tedious works
 beside proof development, tactics writing or documentation.
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 0c8cd408f..b7b343112 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -1,6 +1,7 @@
 \newtheorem{cscexample}{Example}
 
 \achapter{\protect{Generalized rewriting}}
+%HEVEA\cutname{setoid.html}
 \aauthor{Matthieu Sozeau}
 \label{setoids}
 
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 6ea253739..75fac9454 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -1,4 +1,5 @@
 \achapter{Polymorphic Universes}
+%HEVEA\cutname{universes.html}
 \aauthor{Matthieu Sozeau}
 
 \label{Universes-full}