diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-07-07 17:53:54 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-07-07 17:53:54 +0200 |
| commit | f29b968c54889dd82fd07d50bc6a52b63ea4edf0 (patch) | |
| tree | 43edeb072338b9286725c6d6d07535611bc43232 | |
| parent | 3264fdaa71b2327a992286a08df0dfbcf78ea4fe (diff) | |
Document Set/Print Firstorder Solver option.
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index be82eaa01..8f9ba1ec6 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}} |