diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-14 23:07:49 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-14 23:07:49 +0100 |
| commit | b92d5a32c314eee0c68a70c33f1847545aabeb19 (patch) | |
| tree | e18ebcbdf377d5e3dbd7ffe1224539309baa7086 /riscV/Asmgenproof.v | |
| parent | d7c9c729ba52ae926238ab97650104117e488c05 (diff) | |
| download | compcert-kvx-b92d5a32c314eee0c68a70c33f1847545aabeb19.tar.gz compcert-kvx-b92d5a32c314eee0c68a70c33f1847545aabeb19.zip | |
64-bit signed division by two code
Diffstat (limited to 'riscV/Asmgenproof.v')
| -rw-r--r-- | riscV/Asmgenproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 1f3f80d7..63287a50 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -290,7 +290,7 @@ Opaque Int.eq. - apply opimm64_label; intros; exact I. - apply opimm64_label; intros; exact I. - apply opimm64_label; intros; exact I. -- destruct (Int.eq n Int.zero); TailNoLabel. +- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. - eapply transl_cond_op_label; eauto. Qed. |