diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 9 |
2 files changed, 10 insertions, 0 deletions
@@ -247,6 +247,7 @@ Tactics matching lemma among the components of the conjunction; tactic apply also able to apply lemmas of conclusion an empty type. - Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)". +- New tactic "instantiate" (without argument). - Tactic firstorder "with" and "using" options have their meaning swapped for consistency with auto/eauto (source of incompatibility). - Tactic "generalize" now supports "at" options to specify occurrences diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index ffee048d12..7bdc35cf8e 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -833,6 +833,15 @@ in every session. These allow to refer respectively to existential variables occurring in a hypothesis or in the body or the type of a local definition. + \item {\tt instantiate} + + Without argument, the {\tt instantiate} tactic tries to solve as + many existential variables as possible, using information gathered + from other tactics in the same tactical. This is automatically + done after each complete tactic (i.e. after a dot in proof mode), + but not, for example, between each tactic when they are sequenced + by semicolons. + \end{Variants} \subsection{Bindings list |