diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-11-11 14:24:33 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-11-11 14:24:33 +0000 |
commit | a3bc7b24d5f21b99a37a529d06707c5f0e550679 (patch) | |
tree | b450c9693449e7f080ae3f0f9707ffa89e2f0f89 /lib/Integers.v | |
parent | 7a3338431e5f09a90bfda16350202f5c7780d110 (diff) | |
download | compcert-a3bc7b24d5f21b99a37a529d06707c5f0e550679.tar.gz compcert-a3bc7b24d5f21b99a37a529d06707c5f0e550679.zip |
Petites adaptations pour Coq 8.1gamma
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Integers.v')
-rw-r--r-- | lib/Integers.v | 36 |
1 files changed, 22 insertions, 14 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index 5a18dc0c..4eb95845 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -1787,26 +1787,34 @@ End REFLECTION. Remark modu_and_masks_1: forall logn, 0 <= unsigned logn < Z_of_nat wordsize -> rol (shru mone logn) logn = shl mone logn. -Proof (equal_on_range - (fun l => rol (shru mone l) l) - (fun l => shl mone l) - (refl_equal true)). +Proof. + apply (equal_on_range + (fun l => rol (shru mone l) l) + (fun l => shl mone l)). + vm_compute; auto. +Qed. + Remark modu_and_masks_2: forall logn, 0 <= unsigned logn < Z_of_nat wordsize -> and (shl mone logn) (sub (repr (two_p (unsigned logn))) one) = zero. -Proof (equal_on_range - (fun l => and (shl mone l) - (sub (repr (two_p (unsigned l))) one)) - (fun l => zero) - (refl_equal true)). +Proof. + apply (equal_on_range + (fun l => and (shl mone l) + (sub (repr (two_p (unsigned l))) one)) + (fun l => zero)). + vm_compute; auto. +Qed. + Remark modu_and_masks_3: forall logn, 0 <= unsigned logn < Z_of_nat wordsize -> or (shl mone logn) (sub (repr (two_p (unsigned logn))) one) = mone. -Proof (equal_on_range - (fun l => or (shl mone l) - (sub (repr (two_p (unsigned l))) one)) - (fun l => mone) - (refl_equal true)). +Proof. + apply (equal_on_range + (fun l => or (shl mone l) + (sub (repr (two_p (unsigned l))) one)) + (fun l => mone)). + vm_compute; auto. +Qed. Theorem modu_and: forall x n logn, |