From 7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 19 Aug 2011 09:13:09 +0000 Subject: Cleaned up old commented-out parts git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgen.v | 27 +-------------------------- 1 file changed, 1 insertion(+), 26 deletions(-) (limited to 'cfrontend/Cshmgen.v') diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 9856b9e..bbd4cfe 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -209,32 +209,7 @@ Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type end. (** [make_cast from to e] applies to [e] the numeric conversions needed - to transform a result of type [from] to a result of type [to]. - It is decomposed in two functions: -- [make_cast1] converts from integers to floats or from floats to integers; -- [make_cast2] converts to a "small" int or float type if necessary. -*) -(* -Definition make_cast1 (from to: type) (e: expr) := - match from, to with - | Tint _ uns, Tfloat _ => make_floatofint e uns - | Tfloat _, Tint _ uns => make_intoffloat e uns - | _, _ => e - end. - -Definition make_cast2 (from to: type) (e: expr) := - match to with - | Tint I8 Signed => Eunop Ocast8signed e - | Tint I8 Unsigned => Eunop Ocast8unsigned e - | Tint I16 Signed => Eunop Ocast16signed e - | Tint I16 Unsigned => Eunop Ocast16unsigned e - | Tfloat F32 => Eunop Osingleoffloat e - | _ => e - end. - -Definition make_cast (from to: type) (e: expr) := - make_cast2 from to (make_cast1 from to e). -*) + to transform a result of type [from] to a result of type [to]. *) Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) := match sz, si with -- cgit v1.2.3