summaryrefslogtreecommitdiff
path: root/cfrontend/Cshmgenproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/Cshmgenproof.v')
-rw-r--r--cfrontend/Cshmgenproof.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 1089b6b..0b8b9a0 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -1216,8 +1216,6 @@ Proof.
constructor; auto.
(* addrof *)
simpl in TR. auto.
-(* sizeof *)
- constructor; auto.
(* unop *)
eapply transl_unop_correct; eauto.
(* binop *)