summaryrefslogtreecommitdiff
path: root/cfrontend/Csyntax.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/Csyntax.v')
-rw-r--r--cfrontend/Csyntax.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index ea1bd86..a926bc3 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -166,7 +166,7 @@ Inductive statement : Type :=
with labeled_statements : Type := (**r cases of a [switch] *)
| LSnil: labeled_statements
- | LScons: option int -> statement -> labeled_statements -> labeled_statements.
+ | LScons: option Z -> statement -> labeled_statements -> labeled_statements.
(**r [None] is [default], [Some x] is [case x] *)
(** ** Functions *)