diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2019-04-24 14:02:32 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-04-26 13:59:17 +0200 |
| commit | 08fd5faf30c18e17caa610076e67cf002a01d8b4 (patch) | |
| tree | f88a2e1b3de21ebb748850c1b8bf13f3d715979e /arm/Asmgenproof1.v | |
| parent | 51c497b2e5a2b09788f2cf05f414634b037f52bf (diff) | |
| download | compcert-kvx-08fd5faf30c18e17caa610076e67cf002a01d8b4.tar.gz compcert-kvx-08fd5faf30c18e17caa610076e67cf002a01d8b4.zip | |
Move Z definitions out of Integers and into Zbits
The module Integers.Make contained lots of definitions and theorems
about Z integers that were independent of the word size. These
definitions and theorems are useful outside Integers.Make, but
it felt unnatural to fetch them from modules Int or Int64.
This commit moves the word-size-independent definitions and theorems
to a new module, lib/Zbits.v, and fixes their uses in the code base.
Diffstat (limited to 'arm/Asmgenproof1.v')
| -rw-r--r-- | arm/Asmgenproof1.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 98cd5eea..edf35bb8 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -16,6 +16,7 @@ Require Import Coqlib. Require Import Errors. Require Import Maps. Require Import AST. +Require Import Zbits. Require Import Integers. Require Import Floats. Require Import Values. @@ -355,7 +356,7 @@ Proof. rewrite Int.and_assoc. change 65535 with (two_p 16 - 1). rewrite Int.and_idem. apply Int.same_bits_eq; intros. rewrite Int.bits_or, Int.bits_and, Int.bits_shl, Int.testbit_repr by auto. - rewrite Int.Ztestbit_two_p_m1 by omega. change (Int.unsigned (Int.repr 16)) with 16. + rewrite Ztestbit_two_p_m1 by omega. change (Int.unsigned (Int.repr 16)) with 16. destruct (zlt i 16). rewrite andb_true_r, orb_false_r; auto. rewrite andb_false_r; simpl. rewrite Int.bits_shru by omega. |