Petites adaptations pour Coq 8.1gamma

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@135 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

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.