summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-11-11 14:24:33 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-11-11 14:24:33 +0000
commita3bc7b24d5f21b99a37a529d06707c5f0e550679 (patch)
treeb450c9693449e7f080ae3f0f9707ffa89e2f0f89
parent7a3338431e5f09a90bfda16350202f5c7780d110 (diff)
Petites adaptations pour Coq 8.1gamma
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--.depend3
-rw-r--r--Makefile2
-rw-r--r--backend/Registers.v1
-rw-r--r--lib/Coqlib.v1
-rw-r--r--lib/Floats.v2
-rw-r--r--lib/Inclusion.v1
-rw-r--r--lib/Integers.v36
-rw-r--r--lib/Sets.v1
8 files changed, 27 insertions, 20 deletions
diff --git a/.depend b/.depend
index 3404a4a..1571fa7 100644
--- a/.depend
+++ b/.depend
@@ -2,12 +2,11 @@ lib/Coqlib.vo: lib/Coqlib.v
lib/Maps.vo: lib/Maps.v lib/Coqlib.vo
lib/Sets.vo: lib/Sets.v lib/Coqlib.vo lib/Maps.vo lib/Lattice.vo
lib/union_find.vo: lib/union_find.v
-lib/Inclusion.vo: lib/Inclusion.v
lib/Lattice.vo: lib/Lattice.v lib/Coqlib.vo lib/Maps.vo
lib/Ordered.vo: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo
lib/Iteration.vo: lib/Iteration.v lib/Coqlib.vo
lib/Integers.vo: lib/Integers.v lib/Coqlib.vo
-lib/Floats.vo: lib/Floats.v lib/Integers.vo
+lib/Floats.vo: lib/Floats.v lib/Coqlib.vo lib/Integers.vo
lib/Parmov.vo: lib/Parmov.v lib/Coqlib.vo
common/AST.vo: common/AST.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo
common/Events.vo: common/Events.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo
diff --git a/Makefile b/Makefile
index 51e2fa2..91814a0 100644
--- a/Makefile
+++ b/Makefile
@@ -7,7 +7,7 @@ INCLUDES=-I lib -I common -I backend -I cfrontend
# Files in lib/
-LIB=Coqlib.v Maps.v Sets.v union_find.v Inclusion.v Lattice.v Ordered.v \
+LIB=Coqlib.v Maps.v Sets.v union_find.v Lattice.v Ordered.v \
Iteration.v Integers.v Floats.v Parmov.v
# Files in common/
diff --git a/backend/Registers.v b/backend/Registers.v
index 3093589..5b1c723 100644
--- a/backend/Registers.v
+++ b/backend/Registers.v
@@ -4,7 +4,6 @@
intermediate language, and of mappings from pseudo-registers to
values as used in the dynamic semantics of RTL. *)
-Require Import Bool.
Require Import Coqlib.
Require Import AST.
Require Import Maps.
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index b5d59b8..0fc8613 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -4,6 +4,7 @@
Require Export ZArith.
Require Export List.
+Require Export Bool.
Require Import Wf_nat.
(** * Logical axioms *)
diff --git a/lib/Floats.v b/lib/Floats.v
index 67b0e53..f4c5119 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -5,7 +5,7 @@
simply axiomatize a type [float] for IEEE double-precision floats
and the associated operations. *)
-Require Import Bool.
+Require Import Coqlib.
Require Import Integers.
Parameter float: Set.
diff --git a/lib/Inclusion.v b/lib/Inclusion.v
index 1df7517..15e37c4 100644
--- a/lib/Inclusion.v
+++ b/lib/Inclusion.v
@@ -22,6 +22,7 @@ A second tactic, [incl_tac], handles goals of the form
*)
Require Import List.
+Require Import Bool.
Require Import ArithRing.
Ltac all_app e :=
diff --git a/lib/Integers.v b/lib/Integers.v
index 5a18dc0..4eb9584 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,
diff --git a/lib/Sets.v b/lib/Sets.v
index bfc49b1..0a809fc 100644
--- a/lib/Sets.v
+++ b/lib/Sets.v
@@ -9,7 +9,6 @@
implementation of sets.
*)
-Require Import Relations.
Require Import Coqlib.
Require Import Maps.
Require Import Lattice.