Petites adaptations pour Coq 8.1gamma

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

5 files changed, 25 insertions, 16 deletions

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.