diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Asmgenproof0.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index f6f03868..b1b7453a 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -39,12 +39,14 @@ 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 = FR r'. + forall r r', freg_of r = OK r' -> preg_of r = IR 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. |