diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-06 14:33:19 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-06 14:33:19 +0000 |
commit | fafd64a1322205c3c4e3cae0680e03ea341b1cd8 (patch) | |
tree | e0db223602c910fe3505c4c04d187e7df6c49302 /doc/refman | |
parent | d0247bff4b87ce21c2604bfe44af6a16952382e7 (diff) |
Document changes and add missing documentation for Program options.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16563 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman')
-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 |