diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Coercion.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/Coercion.tex b/doc/Coercion.tex index f5c9b2748..13e4cd447 100644 --- a/doc/Coercion.tex +++ b/doc/Coercion.tex @@ -195,7 +195,7 @@ valid coercion paths are ignored; they are signaled by a warning. \texttt{Definition {\ident} : {\type} := {\term}}, and then declares {\ident} as a coercion between it source and its target. -\item {\tt Coercion Local {\ident} := {\term}}\comindex{Local Coercion}\\ +\item {\tt Coercion Local {\ident} := {\term}}\comindex{Coercion Local}\\ This defines {\ident} just like \texttt{Local {\ident} := {\term}}, and then declares {\ident} as a coercion between it source and its target. |