diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-01 13:10:15 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-01 13:10:15 +0000 |
| commit | d9bf805575e6c73dee1d8142f21080ca3e6b57a8 (patch) | |
| tree | e76e4f858fecb7d8f4f47161cd109d8dd1dd502a /doc/refman/Program.tex | |
| parent | 2a5562fa9f003e6bced4f0e4de0a2208cec062a9 (diff) | |
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
Diffstat (limited to 'doc/refman/Program.tex')
| -rw-r--r-- | doc/refman/Program.tex | 3 |
1 files changed, 3 insertions, 0 deletions
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 |