diff options
Diffstat (limited to 'cfrontend/Csyntax.v')
| -rw-r--r-- | cfrontend/Csyntax.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 6c333aa..8b98556 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -165,9 +165,9 @@ Inductive statement : Type := | Sgoto : label -> statement with labeled_statements : Type := (**r cases of a [switch] *) - | LSdefault: statement -> labeled_statements - | LScase: int -> statement -> labeled_statements -> labeled_statements. - + | LSnil: labeled_statements + | LScons: option int -> statement -> labeled_statements -> labeled_statements. + (**r [None] is [default], [Some x] is [case x] *) (** ** Functions *) (** A function definition is composed of its return type ([fn_return]), |