diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-25 09:42:02 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-25 09:42:02 +0200 |
| commit | b66d6034fb09e6129ca24dd458fbef49e4cb98d7 (patch) | |
| tree | 6de73915c6be801e8773c43a3ff4e4252b45d8a1 | |
| parent | 9c29503c6dbfee3c29c70b4ec8fed64b8ec2376a (diff) | |
| download | compcert-kvx-b66d6034fb09e6129ca24dd458fbef49e4cb98d7.tar.gz compcert-kvx-b66d6034fb09e6129ca24dd458fbef49e4cb98d7.zip | |
some progress
| -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. |