diff options
| author | Pierre-Marie Pédrot | 2016-01-21 16:45:23 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-21 16:45:23 +0100 |
| commit | be0eca32fae93ed4793c2f839bb9e725b6a963d1 (patch) | |
| tree | c2c5dce5ce24f5a2a8cade9e69410599c00e2b55 /doc/refman/RefMan-ext.tex | |
| parent | 9c2662eecc398f38be3b6280a8f760cc439bc31c (diff) | |
| parent | 5e23fb90b39dfa014ae5c4fb46eb713cca09dbff (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index f2ab79dced..51e881bff4 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -2014,7 +2014,7 @@ variables, use Instead of letting the unification engine try to solve an existential variable by itself, one can also provide an explicit hole together with a tactic to solve -it. Using the syntax {\tt \textdollar(\expr)\textdollar}, the user can put a +it. Using the syntax {\tt ltac:(\expr)}, the user can put a tactic anywhere a term is expected. The order of resolution is not specified and is implementation-dependent. The inner tactic may use any variable defined in its scope, including repeated alternations between variables introduced by term |