diff options
Diffstat (limited to 'doc/index.html')
| -rw-r--r-- | doc/index.html | 2 |
1 files changed, 1 insertions, 1 deletions
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. |