From af5eafaee218935c35f0bd906727d2d2370bd136 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 20 Jan 2016 15:57:24 +0100
Subject: Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.

---
 doc/refman/RefMan-ext.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3