From fafd64a1322205c3c4e3cae0680e03ea341b1cd8 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 6 Jun 2013 14:33:19 +0000
Subject: 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
---
 doc/refman/Program.tex | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'doc/refman/Program.tex')

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 5632aac42a..193c9d16a3 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
-- 
cgit v1.2.3