From 3d7be6474fe173ceb8094cda06fc752a68a88651 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 27 Sep 2001 13:30:46 +0000
Subject: \} manquant

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8234 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-ext.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3