diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-17 19:22:50 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-17 19:23:05 +0200 |
| commit | fcb7f528c5540d97803a4784234b3aa9c9ebb854 (patch) | |
| tree | 6bd41fb9223e1c073976017855fb18b9dc67dbc8 /doc/index.html | |
| parent | 7a5aef7aa4b669a722ecce3da6e7f7c646a392cc (diff) | |
| download | compcert-kvx-fcb7f528c5540d97803a4784234b3aa9c9ebb854.tar.gz compcert-kvx-fcb7f528c5540d97803a4784234b3aa9c9ebb854.zip | |
Typo in Ctyping entry
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. |