From f29b968c54889dd82fd07d50bc6a52b63ea4edf0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 7 Jul 2015 17:53:54 +0200
Subject: Document Set/Print Firstorder Solver option.

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

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index be82eaa018..8f9ba1ec60 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4164,6 +4164,12 @@ first-order reasoning, written by Pierre Corbineau.
 It is not restricted to usual logical connectives but
 instead may reason about any first-order class inductive definition.
 
+The default tactic used by \texttt{firstorder} when no rule applies is {\tt
+  auto with *}, it can be reset locally or globally using the {\nobreak
+  {\tt Set Firstorder Solver {\tac}}} \optindex{Firstorder Solver}
+vernacular command and printed using {\nobreak {\tt Print Firstorder
+    Solver}}.
+
 \begin{Variants}
  \item {\tt firstorder {\tac}}
    \tacindex{firstorder {\tac}}
-- 
cgit v1.2.3