diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-15 19:49:07 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-15 19:49:07 +0200 |
| commit | 375c844efb8b91d4ff1dce08ed25f55ddef231d7 (patch) | |
| tree | d4c6a7ccfe028e9e7544076fa5f21452b94f2710 /cfrontend | |
| parent | 070babeff47562a72d6a58dd70fc7ac1bcbf205c (diff) | |
| download | compcert-kvx-375c844efb8b91d4ff1dce08ed25f55ddef231d7.tar.gz compcert-kvx-375c844efb8b91d4ff1dce08ed25f55ddef231d7.zip | |
SimplExpr: remove unused definition "sd_cast_set"
Follow-up to commit 070babef.
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 |