Glasnost: making transparent a number of definitions that were opaque

for no good reason.



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

3 files changed, 7 insertions, 5 deletions

diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 7699fef8..658653fb 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -642,7 +642,6 @@ Opaque loadind.
   Simpl. rewrite <- H2. auto.
 
 - (* Mtailcall *)
-Opaque Int.repr.
   assert (f0 = f) by congruence.  subst f0.
   inversion AT; subst.
   assert (NOOV: list_length_z tf <= Int.max_unsigned).
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 1e16a0d4..0e6d3e1c 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -84,7 +84,7 @@ Proof.
   set (x := Int.sub n (low_s n)).
   assert (x = Int.add (Int.mul (Int.divu x (Int.repr 65536)) (Int.repr 65536))
                       (Int.modu x (Int.repr 65536))).
-    apply Int.modu_divu_Euclid. compute; congruence.
+    apply Int.modu_divu_Euclid. vm_compute; congruence.
   assert (Int.modu x (Int.repr 65536) = Int.zero).
     unfold Int.modu, Int.zero. decEq.
     change 0 with (0 mod 65536).
@@ -710,6 +710,7 @@ Proof.
   assert (Int.unsigned (Int.not i) <> Int.modulus - 1).
     red; intros.
     assert (Int.repr (Int.unsigned (Int.not i)) = Int.mone).
+Local Transparent Int.repr.
       rewrite H1. apply Int.mkint_eq. reflexivity. 
    rewrite Int.repr_unsigned in H2. 
    assert (Int.not (Int.not i) = Int.zero).
@@ -813,7 +814,7 @@ Lemma transl_op_correct_aux:
      match op with Omove => data_preg r = true | _ => nontemp_preg r = true end ->
      r <> preg_of res -> rs'#r = rs#r.
 Proof.
-Opaque Int.eq. Opaque Int.repr.
+Opaque Int.eq.
   intros. unfold transl_op in H; destruct op; ArgsInv; simpl in H0; try (inv H0); try TranslOpSimpl.
   (* Omove *)
   destruct (preg_of res) eqn:RES; destruct (preg_of m0) eqn:ARG; inv H.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index a8936fe8..110796ba 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -120,14 +120,16 @@ Proof.
   assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality.
   assert (forall (x y: condition), {x=y}+{x<>y}). decide equality.
   decide equality.
-Qed.
+Defined.
 
 Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}.
 Proof.
   generalize Int.eq_dec; intro.
   assert (forall (x y: ident), {x=y}+{x<>y}). exact peq.
   decide equality.
-Qed.
+Defined.
+
+Global Opaque eq_addressing eq_operation.
 
 (** * Evaluation functions *)