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/Stacklayout.v | |
| parent | 52b4f973646c3b79804fcdddeed5325ab1f3ce7d (diff) | |
| download | compcert-kvx-b2fc9b55d9c59a9c507786a650377e2f0a1ddad8.tar.gz compcert-kvx-b2fc9b55d9c59a9c507786a650377e2f0a1ddad8.zip | |
simpl -> cbn
Diffstat (limited to 'kvx/Stacklayout.v')
| -rw-r--r-- | kvx/Stacklayout.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kvx/Stacklayout.v b/kvx/Stacklayout.v index 46202e03..81ffcebb 100644 --- a/kvx/Stacklayout.v +++ b/kvx/Stacklayout.v @@ -63,7 +63,7 @@ Lemma frame_env_separated: ** P. Proof. Local Opaque Z.add Z.mul sepconj range. - intros; simpl. + intros; cbn. set (w := if Archi.ptr64 then 8 else 4). set (olink := align (4 * b.(bound_outgoing)) w). set (oretaddr := olink + w). @@ -105,7 +105,7 @@ Lemma frame_env_range: let fe := make_env b in 0 <= fe_stack_data fe /\ fe_stack_data fe + bound_stack_data b <= fe_size fe. Proof. - intros; simpl. + intros; cbn. set (w := if Archi.ptr64 then 8 else 4). set (olink := align (4 * b.(bound_outgoing)) w). set (oretaddr := olink + w). @@ -133,7 +133,7 @@ Lemma frame_env_aligned: /\ (align_chunk Mptr | fe_ofs_link fe) /\ (align_chunk Mptr | fe_ofs_retaddr fe). Proof. - intros; simpl. + intros; cbn. set (w := if Archi.ptr64 then 8 else 4). set (olink := align (4 * b.(bound_outgoing)) w). set (oretaddr := olink + w). |