aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Initializers.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/Initializers.v')
-rw-r--r--cfrontend/Initializers.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index 388b6544..77d6cfea 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -186,7 +186,7 @@ Fixpoint transl_init_rec (ce: composite_env) (ty: type) (i: initializer)
| Init_single a, _ =>
do d <- transl_init_single ce ty a; OK (d :: k)
| Init_array il, Tarray tyelt nelt _ =>
- transl_init_array ce tyelt il (Zmax 0 nelt) k
+ transl_init_array ce tyelt il (Z.max 0 nelt) k
| Init_struct il, Tstruct id _ =>
do co <- lookup_composite ce id;
match co_su co with