From 8d5c6bb8f0cac1339dec7b730997ee30b1517073 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 22 Sep 2017 19:50:52 +0200 Subject: Remove coq warnings (#28) Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts. --- cfrontend/Cminorgen.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cfrontend/Cminorgen.v') 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. -- cgit