diff options
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 |