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, 8 insertions, 5 deletions

diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index 860f04c..060d018 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -879,8 +879,8 @@ Opaque loadind.
   intros [m3' [P Q]].
   left; econstructor; split.
   apply plus_one. econstructor; eauto. 
-  subst x; simpl. eauto.
-Opaque Int.repr. 
+  subst x; simpl.
+  rewrite Int.unsigned_zero. simpl. eauto.
   simpl. rewrite C. simpl in F. rewrite (sp_val _ _ _ AG) in F. rewrite F.
   simpl in P. rewrite ATLR. rewrite P. eauto.
   econstructor; eauto.
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index 9935efa..df96393 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -40,7 +40,8 @@ Inductive mreg: Type :=
   | FT1: mreg (* X6 *) | FT2: mreg (* X7 *) | FP0: mreg (* top of FP stack *).
 
 Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}.
-Proof. decide equality. Qed.
+Proof. decide equality. Defined.
+Global Opaque mreg_eq.
 
 Definition mreg_type (r: mreg): typ :=
   match r with
diff --git a/ia32/Op.v b/ia32/Op.v
index 66ee633..a23e8ac 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -124,7 +124,7 @@ Proof.
   generalize Int.eq_dec; intro.
   assert (forall (x y: ident), {x=y}+{x<>y}). exact peq.
   decide equality.
-Qed.
+Defined.
 
 Definition eq_operation (x y: operation): {x=y} + {x<>y}.
 Proof.
@@ -135,7 +135,9 @@ Proof.
   assert (forall (x y: condition), {x=y}+{x<>y}). decide equality.
   decide equality.
   apply eq_addressing.
-Qed.
+Defined.
+
+Global Opaque eq_addressing eq_operation.
 
 (** * Evaluation functions *)