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

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