diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-19 17:07:32 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-20 15:21:27 +0100 |
| commit | 1af878e0dac2198ae487d0b37438520772f28350 (patch) | |
| tree | 1865cbe2a0e2a7b7485cc73f6d1c4abeb4010d63 /doc | |
| parent | 281e4cb8b04c7fd13ec6416e4dcd05ffa1f48761 (diff) | |
Documenting Set Bullet Behavior.
This is useful for restoring bullets after e.g. loading ssreflect.
Hoping Arnaud is ok in documenting it.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index ed1b79e56..c37367de5 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} |