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. --- powerpc/SelectLongproof.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'powerpc/SelectLongproof.v') diff --git a/powerpc/SelectLongproof.v b/powerpc/SelectLongproof.v index a214d131..f16c967e 100644 --- a/powerpc/SelectLongproof.v +++ b/powerpc/SelectLongproof.v @@ -12,7 +12,7 @@ (** Correctness of instruction selection for 64-bit integer operations *) -Require Import String Coqlib Maps Integers Floats Errors. +Require Import String Coqlib Maps Zbits Integers Floats Errors. Require Archi. Require Import AST Values Memory Globalenvs Events. Require Import Cminor Op CminorSel. @@ -221,11 +221,11 @@ Proof. change (Int64.unsigned Int64.iwordsize) with 64. f_equal. rewrite Int.unsigned_repr. - apply Int.eqmod_mod_eq. omega. - apply Int.eqmod_trans with a. - apply Int.eqmod_divides with Int.modulus. apply Int.eqm_sym. apply Int.eqm_unsigned_repr. + apply eqmod_mod_eq. omega. + apply eqmod_trans with a. + apply eqmod_divides with Int.modulus. apply Int.eqm_sym. apply Int.eqm_unsigned_repr. exists (two_p (32-6)); auto. - apply Int.eqmod_divides with Int64.modulus. apply Int64.eqm_unsigned_repr. + apply eqmod_divides with Int64.modulus. apply Int64.eqm_unsigned_repr. exists (two_p (64-6)); auto. assert (0 <= Int.unsigned (Int.repr a) mod 64 < 64) by (apply Z_mod_lt; omega). assert (64 < Int.max_unsigned) by (compute; auto). -- cgit