diff options
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 2c38ffae..954ffba2 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -358,7 +358,11 @@ Proof. (Int.add n (Int.sub Int.iwordsize (Int.add n1 Int.one))) Int.one) Int.iwordsize))) with n. constructor. - ** + ** repeat (try rewrite Int.add_signed; try rewrite Int.sub_signed; try rewrite Int.signed_repr). + rewrite <- (Int.repr_signed n) at 1. + f_equal. + omega. + - TrivialExists. - intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto. |