diff options
| author | Matej Kosik | 2015-12-16 15:44:14 +0100 |
|---|---|---|
| committer | Matej Kosik | 2015-12-18 15:58:36 +0100 |
| commit | 84f54fd0923c15109910123443348c193e37fe0f (patch) | |
| tree | f48efbf8c300fb063f6e0b9fc000d28db9174250 | |
| parent | 493b5d18971c8c19eaeccfc992d1212c6479d227 (diff) | |
TYPOGRAPHY: correction of one particular error in the Reference Manual
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
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. |