Tweaks to support defunctorization.

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

1 files changed, 19 insertions, 9 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index 4464d26..a3ff520 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -421,7 +421,7 @@ Qed.
 Remark half_modulus_modulus: modulus = 2 * half_modulus.
 Proof.
   rewrite half_modulus_power. rewrite modulus_power. 
-  rewrite <- two_p_S. decEq. omega. 
+  rewrite <- two_p_S. apply f_equal. omega. 
   generalize wordsize_pos; omega.
 Qed.
 
@@ -1016,8 +1016,6 @@ Proof.
   rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega. 
 Qed. 
 
-
-
 (** ** Properties of multiplication *)
 
 Theorem mul_commut: forall x y, mul x y = mul y x.
@@ -2057,7 +2055,7 @@ Qed.
 Lemma ltu_iwordsize_inv:
   forall x, ltu x iwordsize = true -> 0 <= unsigned x < zwordsize.
 Proof.
-  intros. exploit ltu_inv; eauto. rewrite unsigned_repr_wordsize. auto.
+  intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize. auto.
 Qed.
 
 Theorem shl_shl:
@@ -2331,7 +2329,7 @@ Theorem shl_rolm:
   ltu n iwordsize = true ->
   shl x n = rolm x n (shl mone n).
 Proof.
-  intros. exploit ltu_inv; eauto. rewrite unsigned_repr_wordsize; intros.
+  intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize; intros.
   unfold rolm. apply same_bits_eq; intros. 
   rewrite bits_and; auto. rewrite !bits_shl; auto. rewrite bits_rol; auto. 
   destruct (zlt i (unsigned n)).
@@ -2347,7 +2345,7 @@ Theorem shru_rolm:
   ltu n iwordsize = true ->
   shru x n = rolm x (sub iwordsize n) (shru mone n).
 Proof.
-  intros. exploit ltu_inv; eauto. rewrite unsigned_repr_wordsize; intros.
+  intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize; intros.
   unfold rolm. apply same_bits_eq; intros. 
   rewrite bits_and; auto. rewrite !bits_shru; auto. rewrite bits_rol; auto. 
   destruct (zlt (i + unsigned n) zwordsize).
@@ -2852,7 +2850,7 @@ Proof.
   intros.
   set (uy := unsigned y).
   assert (0 <= uy < zwordsize - 1).
-    exploit ltu_inv; eauto. rewrite unsigned_repr. auto. 
+    generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto. 
     generalize wordsize_pos wordsize_max_unsigned; omega.
   rewrite shr_div_two_p. unfold shrx. unfold divs.  
   assert (shl one y = repr (two_p uy)).
@@ -2896,7 +2894,7 @@ Proof.
 - set (uy := unsigned y).
   generalize (unsigned_range y); fold uy; intros.
   assert (0 <= uy < zwordsize - 1).
-    exploit ltu_inv; eauto. rewrite unsigned_repr. auto. 
+    generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto. 
     generalize wordsize_pos wordsize_max_unsigned; omega.
   assert (two_p uy < modulus).
     rewrite modulus_power. apply two_p_monotone_strict. omega. 
@@ -2937,7 +2935,7 @@ Proof.
   2: rewrite add_zero; auto.
   set (uy := unsigned y).
   assert (0 <= uy < zwordsize - 1).
-    exploit ltu_inv; eauto. rewrite unsigned_repr. auto.
+    generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto.
     generalize wordsize_pos wordsize_max_unsigned; omega.
   assert (shl one y = repr (two_p uy)).
     rewrite shl_mul_two_p. rewrite mul_commut. apply mul_one.
@@ -3828,8 +3826,12 @@ Module Wordsize_32.
   Proof. unfold wordsize; congruence. Qed.
 End Wordsize_32.
 
+Strategy opaque [Wordsize_32.wordsize].
+
 Module Int := Make(Wordsize_32).
 
+Strategy 0 [Wordsize_32.wordsize].
+
 Notation int := Int.int.
 
 Remark int_wordsize_divides_modulus:
@@ -3844,8 +3846,12 @@ Module Wordsize_8.
   Proof. unfold wordsize; congruence. Qed.
 End Wordsize_8.
 
+Strategy opaque [Wordsize_8.wordsize].
+
 Module Byte := Make(Wordsize_8).
 
+Strategy 0 [Wordsize_8.wordsize].
+
 Notation byte := Byte.int.
 
 Module Wordsize_64.
@@ -3854,6 +3860,8 @@ Module Wordsize_64.
   Proof. unfold wordsize; congruence. Qed.
 End Wordsize_64.
 
+Strategy opaque [Wordsize_64.wordsize].
+
 Module Int64.
 
 Include Make(Wordsize_64).
@@ -4423,6 +4431,8 @@ Qed.
 
 End Int64.
 
+Strategy 0 [Wordsize_64.wordsize].
+
 Notation int64 := Int64.int.
 
 Global Opaque Int.repr Int64.repr Byte.repr.