diff --git a/doc/index.html b/doc/index.html index 857457cbae..10b30c3e9d 100644 --- a/doc/index.html +++ b/doc/index.html @@ -25,11 +25,11 @@
CompCert is a compiler that generates PowerPC, ARM, RISC-V and x86 assembly +
CompCert is a compiler that generates ARM, PowerPC, RISC-V and x86 assembly code from CompCert C, a large subset of the C programming language. The particularity of this compiler is that it is written mostly within the specification language of the Coq proof assistant, and its