diff options
| -rw-r--r-- | mppa_k1c/Chunks.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/mppa_k1c/Chunks.v b/mppa_k1c/Chunks.v index 833f8116..40778877 100644 --- a/mppa_k1c/Chunks.v +++ b/mppa_k1c/Chunks.v @@ -1,10 +1,12 @@ Require Import AST. Require Import Values. Require Import Integers. +Require Import Coq.ZArith.BinIntDef. +Require Import BinNums. Local Open Scope Z_scope. -Definition zscale_of_chunk (chunk: memory_chunk) := +Definition zscale_of_chunk (chunk: memory_chunk) : Z := match chunk with | Mint8signed => 0 | Mint8unsigned => 0 |