diff options
Diffstat (limited to 'cfrontend/Csem.v')
| -rw-r--r-- | cfrontend/Csem.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 14b8053..248192c 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -426,7 +426,7 @@ Definition empty_env: env := (PTree.empty block). how the execution terminated: either normally or prematurely through the execution of a [break], [continue] or [return] statement. *) -Inductive outcome: Set := +Inductive outcome: Type := | Out_break: outcome (**r terminated by [break] *) | Out_continue: outcome (**r terminated by [continue] *) | Out_normal: outcome (**r terminated normally *) |