diff options
| author | Hanzhi Liu <55851864+MisakaCenter@users.noreply.github.com> | 2022-04-25 22:36:55 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-04-25 16:36:55 +0200 |
| commit | fb1f4545dfe861ff4d02816e295021a7e3061687 (patch) | |
| tree | 352f8ab1eacc758681239932edaae9eaa895a48d /cfrontend | |
| parent | 967c04de6c02bef349df579cddbfcac8cf262e6d (diff) | |
| download | compcert-fb1f4545dfe861ff4d02816e295021a7e3061687.tar.gz compcert-fb1f4545dfe861ff4d02816e295021a7e3061687.zip | |
Fix a typo in a comment in Clight.v (#427)
`Kloop1` should have been `Kloop2`.
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/Clight.v | 2 |
1 files changed, 1 insertions, 1 deletions
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 *) |