diff options
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index c3ee28f1..19b1b1f1 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -2573,7 +2573,7 @@ Proof. { eapply A2. } { apply exec_straight_one. simpl. rewrite (C2 SP) by auto with asmgen. rewrite <- (sp_val _ _ rs1 AG1). simpl; rewrite LP'. - rewrite FREE'; eauto. (* auto. *) } } + rewrite FREE'. eauto. (* auto. *) } } * split. (* apply agree_nextinstr. *)apply agree_set_other; auto with asmgen. apply agree_change_sp with (Vptr stk soff). apply agree_exten with rs; auto. intros; rewrite C2; auto with asmgen. |