Documenting Set Bullet Behavior.

This is useful for restoring bullets after e.g. loading ssreflect.

Hoping Arnaud is ok in documenting it.

1 files changed, 13 insertions, 0 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index ed1b79e56e..c37367de5b 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -407,6 +407,19 @@ Proof.
 
 \end{ErrMsgs}
 
+The bullet behavior can be controlled by the following commands.
+
+\begin{quote}
+Set Bullet Behavior "None".
+\end{quote}
+
+This makes bullets inactive.
+
+\begin{quote}
+Set Bullet Behavior "Strict Subproofs".
+\end{quote}
+
+This makes bullets active (this is the default behavior).
 
 \section{Requesting information}