From 377ca6da1e6b36d6dbd0fded7b9f8b4c33d19df1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 20 Mar 2014 14:00:18 +0100
Subject: Documenting the Print Strategy command.

---
 doc/refman/RefMan-oth.tex | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index dc2e454f6a..20893dc4e1 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -1111,6 +1111,21 @@ command is prefixed by {\tt Local}. In the latter case, the behavior
 regarding sections and modules is the same as for the {\tt
   Transparent} and {\tt Opaque} commands.
 
+\subsection{{\tt Print Strategy} \qualid{\tt .}\comindex{Print Strategy}\label{PrintStrategy}}
+
+This command prints the strategy currently associated to \qualid{}. It fails if
+\qualid{} is not an unfoldable reference, that is, neither a variable nor a
+constant.
+
+\begin{ErrMsgs}
+\item The reference is not unfoldable.
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt Print Strategies}\comindex{Print Strategies}\\
+  Print all the currently non-transparent strategies.
+\end{Variants}
+
 \subsection{\tt Declare Reduction \ident\ := {\rm\sl convtactic}.}
 
 This command allows to give a short name to a reduction expression,
-- 
cgit v1.2.3