diff options
| author | msozeau | 2013-06-06 14:33:19 +0000 |
|---|---|---|
| committer | msozeau | 2013-06-06 14:33:19 +0000 |
| commit | fafd64a1322205c3c4e3cae0680e03ea341b1cd8 (patch) | |
| tree | e0db223602c910fe3505c4c04d187e7df6c49302 | |
| parent | d0247bff4b87ce21c2604bfe44af6a16952382e7 (diff) | |
Document changes and add missing documentation for Program options.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16563 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |