diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-05-11 17:13:14 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-05-11 17:13:14 +0200 |
| commit | b81dbb863781a5f450cad0b01f90f729fb1a2244 (patch) | |
| tree | 2260b5bb9afbaef9867c472b0149afd9bcf9af8e /backend/Asmgenproof0.v | |
| parent | a44f224bfa7c340188b54b3bd26a61e94567729b (diff) | |
| download | compcert-kvx-b81dbb863781a5f450cad0b01f90f729fb1a2244.tar.gz compcert-kvx-b81dbb863781a5f450cad0b01f90f729fb1a2244.zip | |
MPPA - refactored instructions
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. |