diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-01-20 15:57:24 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-01-20 15:57:24 +0100 |
| commit | af5eafaee218935c35f0bd906727d2d2370bd136 (patch) | |
| tree | 56b71394d5f39aab76b2351687d4a6df277abb7b /doc | |
| parent | 1af878e0dac2198ae487d0b37438520772f28350 (diff) | |
Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.
Diffstat (limited to 'doc')
| -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 f2ab79dce..51e881bff 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 |