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

4 files changed, 9 insertions, 8 deletions

diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index dcae740..0760eb0 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -261,7 +261,7 @@ Qed.
 Remark transl_op_label:
   forall op args r k c, transl_op op args r k = OK c -> tail_nolabel k c.
 Proof.
-Opaque Int.repr Int.eq.
+Opaque Int.eq.
   unfold transl_op; intros; destruct op; TailNoLabel.
   destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
   destruct (ireg_eq x x0 || ireg_eq x x1); TailNoLabel.
@@ -671,7 +671,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 (fn_code tf) <= Int.max_unsigned).
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 9d90d1f..06d6d17 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -813,8 +813,8 @@ Proof.
   split. unfold rs3. Simpl. 
   replace (rs2 (crbit_for_cond cmp)) with (rs1 (crbit_for_cond cmp)).
   destruct (eval_condition cmp rs##(preg_of##args) m) as [[]|]; simpl in *.
-  rewrite B. simpl. Simpl. 
-  rewrite B. simpl. unfold rs2. Simpl.
+  rewrite B. simpl. rewrite Int.eq_false. Simpl. apply Int.one_not_zero.  
+  rewrite B. simpl. rewrite Int.eq_true. unfold rs2. Simpl.
   auto.
   destruct cmp; reflexivity. 
   intros. transitivity (rs2 r). 
diff --git a/arm/Machregs.v b/arm/Machregs.v
index f5b5329..317515c 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -45,7 +45,7 @@ Inductive mreg: Type :=
   | FT1: mreg (* F6 *) | FT2: mreg (* F7 *).
 
 Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}.
-Proof. decide equality. Qed.
+Proof. decide equality. Defined.
 
 Definition mreg_type (r: mreg): typ :=
   match r with
diff --git a/arm/Op.v b/arm/Op.v
index 291d64f..06d0705 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -137,7 +137,7 @@ Proof.
   subst x. rewrite (proof_irr Px Py). left; auto.
   right. red; intro. elim n. inversion H0. auto.
   decide equality.
-Qed.
+Defined.
 
 Definition eq_operation (x y: operation): {x=y} + {x<>y}.
 Proof.
@@ -148,14 +148,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.
   generalize eq_shift; intro.
   decide equality.
-Qed.
+Defined.
+
+Global Opaque eq_shift eq_operation eq_addressing.
 
 (** * Evaluation functions *)