diff options
Diffstat (limited to 'doc/refman/Program.tex')
| -rw-r--r-- | doc/refman/Program.tex | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 5632aac42..193c9d16a 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -256,6 +256,14 @@ tactic is replaced by the default one if not specified. \item {\tt Set Transparent Obligations}\comindex{Set Transparent Obligations} Control whether all obligations should be declared as transparent (the default), or if the system should infer which obligations can be declared opaque. +\item {\tt Set Hide Obligations}\comindex{Set Hide Obligations} + Control whether obligations appearing in the term should be hidden + as implicit arguments of the special constant + \texttt{Program.Tactics.obligation}. +\item {\tt Set Shrink Obligations}\comindex{Set Shrink Obligations} + Control whether obligations defined by tactics should have their + context minimized to the set of variables used in the proof of the + obligation, to avoid unnecessary dependencies. \end{itemize} The module {\tt Coq.Program.Tactics} defines the default tactic for solving |