From 20cb5c46636c5a855efd49ea6459af12211d7bd0 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 20 Feb 2019 15:04:15 +0100 Subject: Remove unnecessary and error prone FR constructor for pregs --- mppa_k1c/Asmblock.v | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'mppa_k1c/Asmblock.v') diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index a582e866..b9c50517 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -65,17 +65,15 @@ Proof. decide equality. Defined. (** basic register *) Inductive preg: Type := - | IR: gpreg -> preg (**r integer registers *) - | FR: gpreg -> preg (**r float registers *) + | IR: gpreg -> preg (**r integer general purpose registers *) | RA: preg | PC: preg . Coercion IR: gpreg >-> preg. -Coercion FR: gpreg >-> preg. Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. -Proof. decide equality. apply ireg_eq. apply freg_eq. Defined. +Proof. decide equality. apply ireg_eq. Defined. Module PregEq. Definition t := preg. @@ -1436,7 +1434,6 @@ Definition data_preg (r: preg) : bool := | IR GPRA => false | IR RTMP => false | IR _ => true - | FR _ => true | PC => false end. -- cgit