diff options
| -rw-r--r-- | doc/RefMan-ext.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex index 8ba8cd4eeb..1085733141 100644 --- a/doc/RefMan-ext.tex +++ b/doc/RefMan-ext.tex @@ -57,7 +57,7 @@ More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, {\tt Record} {\ident} {\tt [} {\params} {\tt ]} \texttt{:} {\sort} := \verb+{+ {\ident$_1$} \texttt{:} {\type$_1$} \verb+;+ {\ident$_2$} \texttt{:=} {\term$_2$} \verb+;+. -{\ident$_3$} \texttt{:} {\type$_3$} \verb+}+ in which case the correctness of {\type$_3$} may rely on the instance {\term$_2$} of {\ident$_2$ and {\term$_2$} in turn may depend on {\ident$_1$}. +{\ident$_3$} \texttt{:} {\type$_3$} \verb+}+ in which case the correctness of {\type$_3$} may rely on the instance {\term$_2$} of {\ident$_2$} and {\term$_2$} in turn may depend on {\ident$_1$}. \Example |