diff options
Diffstat (limited to 'cfrontend/Cminorgenproof.v')
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 5eaf46b..a472e70 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -939,11 +939,11 @@ Proof. inv H0; try discriminate; inv H1; inv H; TrivialOp. inv H0; try discriminate; inv H1; inv H; TrivialOp. inv H0; try discriminate; inv H1; inv H; TrivialOp. - destruct (Int.ltu i0 (Int.repr 32)); inv H1. TrivialOp. + destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialOp. inv H0; try discriminate; inv H1; inv H; TrivialOp. - destruct (Int.ltu i0 (Int.repr 32)); inv H1. TrivialOp. + destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialOp. inv H0; try discriminate; inv H1; inv H; TrivialOp. - destruct (Int.ltu i0 (Int.repr 32)); inv H1. TrivialOp. + destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialOp. inv H0; try discriminate; inv H1; inv H; TrivialOp. inv H0; try discriminate; inv H1; inv H; TrivialOp. inv H0; try discriminate; inv H1; inv H; TrivialOp. |