Petites adaptations pour Coq 8.1gamma

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

1 files changed, 22 insertions, 14 deletions

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,