diff options
Diffstat (limited to 'powerpc/Asmgenproof1.v')
| -rw-r--r-- | powerpc/Asmgenproof1.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 884d5366..20cf9c1d 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1284,7 +1284,9 @@ Proof. reflexivity. + Simpl. rewrite <- (C r1), <- (C r2) by auto. - rewrite B. destruct dir; destruct ob as [[]|]; simpl; auto using Val.lessdef_normalize. + rewrite B, gpr_or_zero_not_zero. + destruct dir; destruct ob as [[]|]; simpl; auto using Val.lessdef_normalize. + destruct dir; intros e; subst; discriminate. + intros. Simpl. Qed. |