diff options
Diffstat (limited to 'cfrontend/Cminorgen.v')
| -rw-r--r-- | cfrontend/Cminorgen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 5017fc8e..45c21f96 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -226,7 +226,7 @@ Definition assign_variable let (id, sz) := id_sz in let (cenv, stacksize) := cenv_stacksize in let ofs := align stacksize (block_alignment sz) in - (PTree.set id ofs cenv, ofs + Zmax 0 sz). + (PTree.set id ofs cenv, ofs + Z.max 0 sz). Definition assign_variables (cenv_stacksize: compilenv * Z) (vars: list (ident * Z)) : compilenv * Z := List.fold_left assign_variable vars cenv_stacksize. |