diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-01-22 16:42:23 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-01-22 16:42:23 +0100 |
| commit | 89e029310d175ee7ddbb157494bac46a08304b19 (patch) | |
| tree | bd516047d1cea2be0141d00c1a18e440f4f368aa /riscV/Asmgenproof.v | |
| parent | 60c15c9d1105dc2e53c17b3fb28ee9cc4716cbc6 (diff) | |
| parent | fd2181ce5f6a3a5ba27349d1642ee4c59a6d9b34 (diff) | |
| download | compcert-kvx-89e029310d175ee7ddbb157494bac46a08304b19.tar.gz compcert-kvx-89e029310d175ee7ddbb157494bac46a08304b19.zip | |
Merge branch 'mppa-work' into mppa-duplicate-oracle
Diffstat (limited to 'riscV/Asmgenproof.v')
| -rw-r--r-- | riscV/Asmgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index e2fafb16..8e9f022c 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -285,12 +285,12 @@ Opaque Int.eq. - apply opimm32_label; intros; exact I. - apply opimm32_label; intros; exact I. - apply opimm32_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. - apply opimm64_label; intros; exact I. - 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. |