diff options
Diffstat (limited to 'backend/Selectionproof.v')
| -rw-r--r-- | backend/Selectionproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 4e67181a..0aa2b6bf 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -50,7 +50,7 @@ Proof. induction 1; simpl. constructor. constructor. - econstructor. eauto. apply eval_negate_condition. auto. + econstructor. eauto. rewrite eval_negate_condition. rewrite H0. auto. econstructor. eauto. destruct vb1; auto. Qed. @@ -124,7 +124,7 @@ Proof. intros. apply is_compare_neq_zero_correct with (negate_condition c). destruct c; simpl in H; simpl; try discriminate; destruct c; simpl; try discriminate; auto. - apply eval_negate_condition; auto. + rewrite eval_negate_condition. rewrite H0. auto. Qed. Lemma eval_condition_of_expr: |