diff options
Diffstat (limited to 'powerpc/SelectOpproof.v')
| -rw-r--r-- | powerpc/SelectOpproof.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 31ddf304..5f87d9b9 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -1038,6 +1038,9 @@ Proof. - subst v. constructor; auto. - inv H. InvEval. simpl in H6; inv H6. constructor; auto. - inv H. InvEval. simpl in H6. inv H6. constructor; auto. +- inv H. repeat constructor; auto. +- inv H. repeat constructor; auto. +- inv H. repeat constructor; auto. - constructor; auto. Qed. |