From 84f54fd0923c15109910123443348c193e37fe0f Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 16 Dec 2015 15:44:14 +0100
Subject: TYPOGRAPHY: correction of one particular error in the Reference
 Manual

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

(limited to 'doc')

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 2f07beb725..cc7e6b53bf 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1101,7 +1101,7 @@ using the syntax:
 {\tt Ltac} {\qualid} {\ident}$_1$ ... {\ident}$_n$ {\tt ::=}
 {\tacexpr}
 \end{quote}
-A previous definition of \qualid must exist in the environment.
+A previous definition of {\qualid} must exist in the environment.
 The new definition will always be used instead of the old one and
 it goes accross module boundaries.
 
-- 
cgit v1.2.3