From fcb7f528c5540d97803a4784234b3aa9c9ebb854 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sun, 17 Jun 2018 19:22:50 +0200
Subject: Typo in Ctyping entry

---
 doc/index.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/index.html')

diff --git a/doc/index.html b/doc/index.html
index 60c4e9a0..41604cd7 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -338,7 +338,7 @@ See also: <A HREF="html/compcert.powerpc.Needcompcert.powerpc.Op.html"><I>NeedOp
 
 The <A HREF="html/compcert.cfrontend.Ctyping.html">type system of CompCert C</A> is fully formalized.  For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions.
 <UL>
-<LI> <A HREF="html/compcert.cfrontend.Ctyping.html">RTLtyping</A>: typing for CompCert C + type-checking functions.
+<LI> <A HREF="html/compcert.cfrontend.Ctyping.html">Ctyping</A>: typing for CompCert C + type-checking functions.
 <LI> <A HREF="html/compcert.backend.RTLtyping.html">RTLtyping</A>: typing for RTL + type
 reconstruction.
 <LI> <A HREF="html/compcert.backend.Lineartyping.html">Lineartyping</A>: typing for Linear.
-- 
cgit