From 9205d8dc7b9e97b6c2f0815fddc5673c21d11089 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 2 Nov 2015 12:26:53 +0100
Subject: Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in
 WG.

---
 doc/refman/RefMan-ext.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/refman/RefMan-ext.tex')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b77118e1f..80e12898f 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1998,7 +1998,7 @@ variables, use
 \end{quote}
 
 \subsection{Solving existential variables using tactics}
-\ttindex{\textdollar( \ldots )\textdollar}
+\ttindex{ltac:( \ldots )}
 
 \def\expr{\textrm{\textsl{tacexpr}}}
 
@@ -2012,7 +2012,7 @@ binding as well as those introduced by tactic binding. The expression {\expr}
 can be any tactic expression as described at section~\ref{TacticLanguage}.
 
 \begin{coq_example*}
-Definition foo (x : nat) : nat := $( exact x )$.
+Definition foo (x : nat) : nat := ltac:(exact x).
 \end{coq_example*}
 
 This construction is useful when one wants to define complicated terms using
-- 
cgit v1.2.3