From 08fd5faf30c18e17caa610076e67cf002a01d8b4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 24 Apr 2019 14:02:32 +0200 Subject: 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. --- riscV/SelectOpproof.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'riscV/SelectOpproof.v') 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. -- cgit