diff options
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index bbca6968..f0b09ef6 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -787,7 +787,7 @@ Proof. destruct ai; simpl; intros; try (rewrite <- BASIC; rewrite Pregmap.gso; auto; discriminate). - destruct i; simpl in BASIC; - unfold compare_long in BASIC; rewrite <- BASIC; + try destruct (negb _); rewrite <- BASIC; repeat rewrite Pregmap.gso; try discriminate; reflexivity. - destruct i; simpl in BASIC. 1,2: rewrite <- BASIC; repeat rewrite Pregmap.gso; try discriminate; reflexivity. @@ -1169,6 +1169,8 @@ Proof. try (destruct_reg_inv); try (inv_matchi); inversion BASIC; clear BASIC; subst; + try (destruct (is_immediate_float64 _)); + try (destruct (is_immediate_float32 _)); eexists; eexists; split; eauto; repeat (eapply match_internal_nextinstr_set_parallel; try congruence); try (econstructor; eauto); |