Merge PR #1079: 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 eee41a6798..856a823de0 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 1609e4a041..30039d4898 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 275e1c2d55..8961b00964 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 a95d8114ff..7ad895f9d8 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 7e07868a38..22c75b4fc8 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 16006a6adf..ec46e1eb58 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 499239b6f3..83e866e9f3 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 4daf98f87a..2617142f5a 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 e953d2f709..ab00fbfe37 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 70e36a5ee9..1401af10f6 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 1610305e75..8025fbe29f 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 77d5928345..d9b8b8c522 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 f60908da6c..1e204dc83d 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 ad795d4064..0dbfe05d48 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 45230fb6e5..9790111f14 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 7af4e9313a..b27a4dc943 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 ef12fe416a..df0cd2b825 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 c6fbd1c538..75f3d18ded 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 2b9e4e6051..f802a35950 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 4ebb484e7c..c8e8443026 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 3ce1d4ecd8..c8e2ae2dde 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 2019a529fe..7c672cf422 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 8f43ebcfbc..60cd8b73a4 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 0c2a18eb2e..991c9745e9 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 eb59ca584e..8f659ded35 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 23a1c9b029..956f308512 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 db794e5a63..be199e0b24 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 d8a353300f..eecb5ac7c0 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 8fbcfdf308..a2d45046b0 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 cb8f916f13..7cdb1a5274 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 f6371f8e5c..ed41e32161 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 0c8cd408f2..b7b343112f 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 6ea2537399..75fac9454a 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}