diff options
Diffstat (limited to 'backend/Asmgenproof0.v')
| -rw-r--r-- | backend/Asmgenproof0.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index b1b7453a..8dfa8828 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -739,7 +739,7 @@ Lemma tail_nolabel_cons: Proof. intros. destruct H0. split. constructor; auto. - intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction. + intros. simpl. rewrite <- H1. destruct i; destruct i; reflexivity || contradiction. Qed. Hint Resolve tail_nolabel_refl: labels. |