diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-29 16:22:18 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-29 17:08:56 +0200 |
| commit | b2fc9b55d9c59a9c507786a650377e2f0a1ddad8 (patch) | |
| tree | b6e835836c78566162d79c83bf353aa555a1d95c /kvx/Asmblockprops.v | |
| parent | 52b4f973646c3b79804fcdddeed5325ab1f3ce7d (diff) | |
| download | compcert-kvx-b2fc9b55d9c59a9c507786a650377e2f0a1ddad8.tar.gz compcert-kvx-b2fc9b55d9c59a9c507786a650377e2f0a1ddad8.zip | |
simpl -> cbn
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. |