diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | doc/refman/Program.tex | 8 |
2 files changed, 13 insertions, 0 deletions
@@ -56,12 +56,17 @@ Tactics independently of the number of ipats, which has itself to be less than the number of new hypotheses (possible source of incompatibilities; former behavior obtainable by "Unset Injection L2R Pattern Order"). +- New tactic "rewrite_strat" for generalized rewriting with user-defined + strategies, subsumming autorewrite. Program - "Solve Obligations using" changed to "Solve Obligations with", consistent with "Proof with". - Program Lemma, Definition now respect automatic introduction. +- Add/document "Set Hide Obligations" (to hide obligations in the final + term inside an implicit argument) and "Set Shrink Obligations" (to + minimize dependencies of obligations defined by tactics). Notations diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 5632aac42a..193c9d16a3 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -256,6 +256,14 @@ tactic is replaced by the default one if not specified. \item {\tt Set Transparent Obligations}\comindex{Set Transparent Obligations} Control whether all obligations should be declared as transparent (the default), or if the system should infer which obligations can be declared opaque. +\item {\tt Set Hide Obligations}\comindex{Set Hide Obligations} + Control whether obligations appearing in the term should be hidden + as implicit arguments of the special constant + \texttt{Program.Tactics.obligation}. +\item {\tt Set Shrink Obligations}\comindex{Set Shrink Obligations} + Control whether obligations defined by tactics should have their + context minimized to the set of variables used in the proof of the + obligation, to avoid unnecessary dependencies. \end{itemize} The module {\tt Coq.Program.Tactics} defines the default tactic for solving |