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 e06e3e70e..c1295349d 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