diff options
Diffstat (limited to 'kvx/Asmblockprops.v')
-rw-r--r-- | kvx/Asmblockprops.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kvx/Asmblockprops.v b/kvx/Asmblockprops.v index bc14b231..c3929be5 100644 --- a/kvx/Asmblockprops.v +++ b/kvx/Asmblockprops.v @@ -53,7 +53,7 @@ Qed. Lemma preg_of_not_SP: forall r, preg_of r <> SP. Proof. - intros. unfold preg_of; destruct r; simpl; congruence. + intros. unfold preg_of; destruct r; cbn; congruence. Qed. Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen. @@ -233,7 +233,7 @@ Proof. destruct (ireg_eq rd2 ra); try discriminate. *) rewrite Pregmap.gso; try discriminate. - simpl in *. + cbn in *. destruct (Mem.loadv _ _ _); try discriminate. destruct (Mem.loadv _ _ _); try discriminate. destruct (Mem.loadv _ _ _); try discriminate. @@ -264,7 +264,7 @@ Lemma exec_store_q_offset_pc_var: exec_store_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. intros. unfold exec_store_q_offset in *. unfold parexec_store_q_offset in *. rewrite Pregmap.gso; try discriminate. - simpl in *. + cbn in *. destruct (gpreg_q_expand _) as [s0 s1]. destruct (Mem.storev _ _ _); try discriminate. destruct (Mem.storev _ _ _); try discriminate. |