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 /backend/SelectDivproof.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 'backend/SelectDivproof.v')
| -rw-r--r-- | backend/SelectDivproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index e660677a..f4ff2c86 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -12,7 +12,7 @@ (** Correctness of instruction selection for integer division *) -Require Import Zquot Coqlib. +Require Import Zquot Coqlib Zbits. Require Import AST Integers Floats Values Memory Globalenvs Events. Require Import Cminor Op CminorSel. Require Import SelectOp SelectOpproof SplitLong SplitLongproof SelectLong SelectLongproof SelectDiv. @@ -378,7 +378,7 @@ Qed. Remark int64_shr'_div_two_p: forall x y, Int64.shr' x y = Int64.repr (Int64.signed x / two_p (Int.unsigned y)). Proof. - intros; unfold Int64.shr'. rewrite Int64.Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega. + intros; unfold Int64.shr'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega. Qed. Lemma divls_mul_shift_gen: @@ -453,7 +453,7 @@ Qed. Remark int64_shru'_div_two_p: forall x y, Int64.shru' x y = Int64.repr (Int64.unsigned x / two_p (Int.unsigned y)). Proof. - intros; unfold Int64.shru'. rewrite Int64.Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega. + intros; unfold Int64.shru'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega. Qed. Theorem divlu_mul_shift: |