summaryrefslogtreecommitdiff
path: root/powerpc
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-03-09 13:35:00 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-03-09 13:35:00 +0000
commit3ffda353b0d92ccd0ff3693ad0be81531c3c0537 (patch)
tree9a07da4e83919d763086e379de161fd4cfe8ab02 /powerpc
parent06c55ab8fa4c0bf59479faf03d30a51c780da36e (diff)
Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1597 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/Asmgenproof.v10
1 files changed, 5 insertions, 5 deletions
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 65c831e..54e454e 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -776,16 +776,16 @@ Proof.
unfold rs1. rewrite nextinstr_inv; auto with ppcgen. auto. congruence.
intros [rs2 [U [V W]]].
exists rs2; split.
- apply exec_straight_step with rs1 m'.
+ apply exec_straight_step with rs1 m'.
simpl. unfold load1. simpl. rewrite gpr_or_zero_not_zero.
rewrite <- (sp_val _ _ _ AG). rewrite A. auto. congruence. auto.
auto.
assert (agree (Regmap.set IT1 Vundef ms) sp rs1).
- unfold rs1. eauto with ppcgen.
+ unfold rs1. change (IR GPR11) with (preg_of IT1). auto with ppcgen.
apply agree_exten_2 with (rs1#(preg_of dst) <- v').
- auto with ppcgen.
- intros. unfold Pregmap.set. destruct (PregEq.eq r (preg_of dst)).
- congruence. auto.
+ auto with ppcgen.
+ intros. unfold Pregmap.set. destruct (PregEq.eq r (preg_of dst)).
+ congruence. auto.
Qed.
Lemma exec_Mop_prop: