diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-08 11:27:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-08 12:02:50 +0200 |
| commit | 9510a3994210f545119ea35cdad43facededb6a2 (patch) | |
| tree | 08dd8bb0dd3f16894ec96b5df332d1bf7bd35a60 /doc/refman/Program.tex | |
| parent | 99e3bdda7572725f929b77f7349d0a1e06294e94 (diff) | |
Documenting the new behaviour of the Shrink Obligations flag.
Diffstat (limited to 'doc/refman/Program.tex')
| -rw-r--r-- | doc/refman/Program.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 8e078e981..efcc84ee9 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -261,7 +261,7 @@ tactic is replaced by the default one if not specified. as implicit arguments of the special constant \texttt{Program.Tactics.obligation}. \item {\tt Set Shrink Obligations}\optindex{Shrink Obligations} - Control whether obligations defined by tactics should have their + Control whether obligations should have their context minimized to the set of variables used in the proof of the obligation, to avoid unnecessary dependencies. \end{itemize} |