diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-31 08:16:51 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-31 08:16:51 +0200 |
| commit | fd09c489f94df50c6579973e85c205ec07d60187 (patch) | |
| tree | 0d0453ffdd536669102f0f7d3f1f676a5a380681 /doc | |
| parent | 2e39ecb491bbd001ecdfba73115bc76e3f53f517 (diff) | |
| download | compcert-kvx-fd09c489f94df50c6579973e85c205ec07d60187.tar.gz compcert-kvx-fd09c489f94df50c6579973e85c205ec07d60187.zip | |
Improving Coqdoc on abstractbb
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/index-kvx.html | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/index-kvx.html b/doc/index-kvx.html index ff3fbc17..4f666cc3 100644 --- a/doc/index-kvx.html +++ b/doc/index-kvx.html @@ -325,7 +325,7 @@ This IR is generic over the processor, even if currently, only used for KVX. <TD>Flattening bundles (only a bureaucratic operation)</TD> <TD>Asmvliw to Asm</TD> <TD><A HREF="html/compcert.kvx.Asmgen.html"><I>Asmgen</I></A></TD> - <TD><A HREF="html/compcert.kvx.Asmgenproof.html"><I>Asmgenproof</I></A></TD> + <TD><A HREF="html/compcert.kvx.Asmgenproof.html"><I>Asmgenproof</I></A> (whole simulation proof from <tt>Mach</tt> to <tt>Asm</tt>)</TD> </TR> </TABLE> |