diff options
Diffstat (limited to 'verilog/Asmgenproof1.v')
| -rw-r--r-- | verilog/Asmgenproof1.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/verilog/Asmgenproof1.v b/verilog/Asmgenproof1.v index 42ab8375..f37b85b4 100644 --- a/verilog/Asmgenproof1.v +++ b/verilog/Asmgenproof1.v @@ -728,9 +728,9 @@ Lemma transl_cond_int64s_correct: Proof. intros. destruct cmp; simpl. - econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto. + split; intros; Simpl. destruct (rs###r1); auto. - econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto. + split; intros; Simpl. destruct (rs###r1); auto. - econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. split; intros; Simpl. - econstructor; split. |