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 /riscV/SelectOpproof.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 'riscV/SelectOpproof.v')
| -rw-r--r-- | riscV/SelectOpproof.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 90f077db..d12bd8af 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -20,6 +20,7 @@ Require Import Coqlib. Require Import Maps. Require Import AST. +Require Import Zbits. Require Import Integers. Require Import Floats. Require Import Values. @@ -372,7 +373,7 @@ Proof. change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl. apply Val.lessdef_same. f_equal. transitivity (Int.repr (Z.shiftr (Int.signed i * Int.signed i0) 32)). - unfold Int.mulhs; f_equal. rewrite Int.Zshiftr_div_two_p by omega. reflexivity. + unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity. apply Int.same_bits_eq; intros n N. change Int.zwordsize with 32 in *. assert (N1: 0 <= n < 64) by omega. @@ -400,7 +401,7 @@ Proof. change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl. apply Val.lessdef_same. f_equal. transitivity (Int.repr (Z.shiftr (Int.unsigned i * Int.unsigned i0) 32)). - unfold Int.mulhu; f_equal. rewrite Int.Zshiftr_div_two_p by omega. reflexivity. + unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity. apply Int.same_bits_eq; intros n N. change Int.zwordsize with 32 in *. assert (N1: 0 <= n < 64) by omega. |