From fb1f4545dfe861ff4d02816e295021a7e3061687 Mon Sep 17 00:00:00 2001
From: Hanzhi Liu <55851864+MisakaCenter@users.noreply.github.com>
Date: Mon, 25 Apr 2022 22:36:55 +0800
Subject: Fix a typo in a comment in Clight.v (#427)

`Kloop1` should have been `Kloop2`.
---
 cfrontend/Clight.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index d15bc90a..a06e9ac3 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -459,7 +459,7 @@ Inductive cont: Type :=
   | Kstop: cont
   | Kseq: statement -> cont -> cont       (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
   | Kloop1: statement -> statement -> cont -> cont (**r [Kloop1 s1 s2 k] = after [s1] in [Sloop s1 s2] *)
-  | Kloop2: statement -> statement -> cont -> cont (**r [Kloop1 s1 s2 k] = after [s2] in [Sloop s1 s2] *)
+  | Kloop2: statement -> statement -> cont -> cont (**r [Kloop2 s1 s2 k] = after [s2] in [Sloop s1 s2] *)
   | Kswitch: cont -> cont       (**r catches [break] statements arising out of [switch] *)
   | Kcall: option ident ->                  (**r where to store result *)
            function ->                      (**r calling function *)
-- 
cgit