diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-05-03 10:43:38 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-05-03 10:43:38 +0200 |
| commit | 6783207fa4282f53af1da8bf09e4819716acde64 (patch) | |
| tree | 8c65b43c911bd4dd59d6f76b26867082bd641515 | |
| parent | 92b48e2aa6d24d1ad487c1d2a3644a57966c765e (diff) | |
| download | compcert-kvx-6783207fa4282f53af1da8bf09e4819716acde64.tar.gz compcert-kvx-6783207fa4282f53af1da8bf09e4819716acde64.zip | |
Fixing mppa_k1c/Chunks.v for Coq 8.9
| -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 |