From 1af878e0dac2198ae487d0b37438520772f28350 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 19 Jan 2016 17:07:32 +0100
Subject: Documenting Set Bullet Behavior.

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

Hoping Arnaud is ok in documenting it.
---
 doc/refman/RefMan-pro.tex | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'doc/refman/RefMan-pro.tex')

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}
 
-- 
cgit v1.2.3