From d9bf805575e6c73dee1d8142f21080ca3e6b57a8 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 1 Apr 2008 13:10:15 +0000
Subject: Add option to set the opacity of obligations to transparent, to be
 able to reduce proofs (requested by users).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10735 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/Program.tex | 3 +++
 1 file changed, 3 insertions(+)

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

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index e06e3e70e1..c1295349da 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -212,6 +212,9 @@ tactic is replaced by the default one if not specified.
   Sets the default obligation
   solving tactic applied to all obligations automatically, whether to
   solve them or when starting to prove one, e.g. using {\tt Next}.
+\item {\tt Set Transparent Obligations}
+  Force all obligations to be declared as transparent, otherwise let the
+  system infer which obligations can be declared opaque.
 \item {\tt Obligations [of \ident]}\comindex{Obligations} Displays all remaining
   obligations.
 \item {\tt Obligation num [of \ident]}\comindex{Obligation} Start the proof of
-- 
cgit v1.2.3

