From 346e961fe93fd62cb00eef80ce42181b5a03c680 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 17 Jun 2002 13:27:24 +0000
Subject: Local Coercion -> Coercion Local (dans l'index)

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

diff --git a/doc/Coercion.tex b/doc/Coercion.tex
index f5c9b2748e..13e4cd4473 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.
-- 
cgit v1.2.3