diff options
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/SimplExpr.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 1398317d..c7e57a54 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -226,8 +226,6 @@ Definition sd_seqbool_val (tmp: ident) (ty: type) := SDbase type_bool ty tmp. Definition sd_seqbool_set (ty: type) (sd: set_destination) := let tmp := sd_temp sd in SDcons type_bool ty tmp sd. -Definition sd_cast_set (ty: type) (sd: set_destination) := - let tmp := sd_temp sd in SDcons ty ty tmp sd. Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement * expr) := match a with |