From a80a8b9ee92c9dd015d53d8de03b99c0d228d390 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 2 Mar 2018 17:19:15 +0100 Subject: MPPA - Started Asm.v + Asmgen.v, commenting out some instructions --- backend/Asmgenproof0.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'backend') 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. -- cgit