From fd09c489f94df50c6579973e85c205ec07d60187 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Fri, 31 Jul 2020 08:16:51 +0200
Subject: Improving Coqdoc on abstractbb

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

(limited to 'doc')

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>
 
-- 
cgit