From 02779dbc71c0f6985427c47ec05dd25b44dd859c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 10 Mar 2013 12:13:12 +0000 Subject: 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 --- powerpc/Asmgenproof.v | 1 - powerpc/Asmgenproof1.v | 5 +++-- powerpc/Op.v | 6 ++++-- 3 files changed, 7 insertions(+), 5 deletions(-) (limited to 'powerpc') 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 *) -- cgit