diff options
| author | herbelin | 2001-09-27 13:30:46 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-27 13:30:46 +0000 |
| commit | 3d7be6474fe173ceb8094cda06fc752a68a88651 (patch) | |
| tree | c6de1aa63f5fb1309ace1783fcfafea90c903f77 | |
| parent | d09eb54a65e2e89936ec79c8c4a693ca5b3c2a97 (diff) | |
\} manquant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8234 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |