3 files changed, 5 insertions, 1 deletions
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex
index a3372c2965..275e1c2d55 100644
--- a/doc/refman/CanonicalStructures.tex
+++ b/doc/refman/CanonicalStructures.tex
@@ -4,7 +4,7 @@
 \label{CS-full}
 \index{Canonical Structures!presentation}
 
-This chapter explains the basics of Canonical Structure and how thy can be used
+\noindent This chapter explains the basics of Canonical Structure and how they can be used
 to overload notations and build a hierarchy of algebraic structures.
 The examples are taken from~\cite{CSwcu}.  We invite the interested reader
 to refer to this paper for all the details that are omitted here for brevity.
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index cc7e6b53bf..12dea9a306 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1116,6 +1116,8 @@ Defined {\ltac} functions can be displayed using the command
 {\tt Print Ltac {\qualid}.}
 \end{quote}
 
+The command {\tt Print Ltac Signatures\comindex{Print Ltac Signatures}} displays a list of all user-defined tactics, with their arguments.
+
 \section{Debugging {\ltac} tactics}
 
 \subsection[Info trace]{Info trace\comindex{Info}\optindex{Info Level}}
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index a12983ab84..fb45777e7f 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -21,6 +21,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Init/Peano.v
     theories/Init/Specif.v
     theories/Init/Tactics.v
+    theories/Init/Tauto.v
     theories/Init/Wf.v
     (theories/Init/Prelude.v)
   </dd>
@@ -203,6 +204,7 @@ through the <tt>Require Import</tt> command.</p>
     (theories/QArith/QArith.v)
     theories/QArith/Qreals.v
     theories/QArith/Qcanon.v
+    theories/QArith/Qcabs.v
     theories/QArith/Qround.v
     theories/QArith/QOrderedType.v
     theories/QArith/Qminmax.v