diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-26 17:35:31 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-26 17:35:31 +0100 |
| commit | 5631ccb7c416bb7ecbe7920cb432a78436c0a7ac (patch) | |
| tree | c84dfc9edea4d1aaf48985a229dddb811cbc3ffa /backend/Asmgenproof0.v | |
| parent | 3d38bf85c8ac3a83fe7aaeb5e01bb9a8403e6a60 (diff) | |
| download | compcert-kvx-5631ccb7c416bb7ecbe7920cb432a78436c0a7ac.tar.gz compcert-kvx-5631ccb7c416bb7ecbe7920cb432a78436c0a7ac.zip | |
BROKEN - works for x86, not for k1 anymore
Diffstat (limited to 'backend/Asmgenproof0.v')
| -rw-r--r-- | backend/Asmgenproof0.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 3e25c79b..70c4323c 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -39,14 +39,12 @@ Proof. unfold ireg_of; intros. destruct (preg_of r); inv H; auto. Qed. -(* FIXME - Replaced FR by IR for MPPA *) Lemma freg_of_eq: - forall r r', freg_of r = OK r' -> preg_of r = IR r'. + forall r r', freg_of r = OK r' -> preg_of r = FR r'. Proof. unfold freg_of; intros. destruct (preg_of r); inv H; auto. Qed. - Lemma preg_of_injective: forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2. Proof. @@ -756,7 +754,7 @@ Lemma tail_nolabel_cons: Proof. intros. destruct H0. split. constructor; auto. - intros. simpl. rewrite <- H1. destruct i; destruct i; reflexivity || contradiction. + intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction. Qed. Hint Resolve tail_nolabel_refl: labels. |