aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--kvx/Asmblockgenproof.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/kvx/Asmblockgenproof.v b/kvx/Asmblockgenproof.v
index 5cb498bc..df1a070f 100644
--- a/kvx/Asmblockgenproof.v
+++ b/kvx/Asmblockgenproof.v
@@ -13,7 +13,7 @@
(* *)
(* *************************************************************)
-(** Correctness proof for RISC-V generation: main proof. *)
+(** Correctness proof for kvx/Asmblock generation: main proof. *)
Require Import Coqlib Errors.
Require Import Integers Floats AST Linking.