diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index fc3fdd002..15df2e601 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1337,12 +1337,16 @@ in the list of subgoals remaining to prove. quantifications or non-dependent implications) are instantiated by concrete terms coming either from arguments \term$_1$ $\ldots$ \term$_n$ or from a bindings list (see - Section~\ref{Binding-list} for more about bindings lists). In the - second form, all instantiation elements must be given, whereas - in the first form the application to \term$_1$ {\ldots} + Section~\ref{Binding-list} for more about bindings lists). + In the first form the application to \term$_1$ {\ldots} \term$_n$ can be partial. The first form is equivalent to {\tt assert ({\ident} := {\ident} {\term$_1$} \dots\ \term$_n$)}. + In the second form, instantiation elements can also be partial. + In this case the uninstantiated arguments are inferred by + unification if possible or left quantified in the hypothesis + otherwise. + With the {\tt as} clause, the local hypothesis {\ident} is left unchanged and instead, the modified hypothesis is introduced as specified by the {\intropattern}. |