From 8d5c6bb8f0cac1339dec7b730997ee30b1517073 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bschommer@users.noreply.github.com>
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.
---
 common/AST.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'common/AST.v')

diff --git a/common/AST.v b/common/AST.v
index 9eeca5b1..a072ef29 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -214,7 +214,7 @@ Definition init_data_size (i: init_data) : Z :=
   | Init_float32 _ => 4
   | Init_float64 _ => 8
   | Init_addrof _ _ => if Archi.ptr64 then 8 else 4
-  | Init_space n => Zmax n 0
+  | Init_space n => Z.max n 0
   end.
 
 Fixpoint init_data_list_size (il: list init_data) {struct il} : Z :=
-- 
cgit