From b2fc9b55d9c59a9c507786a650377e2f0a1ddad8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 29 Sep 2020 16:22:18 +0200 Subject: simpl -> cbn --- kvx/Stacklayout.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kvx/Stacklayout.v') 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). -- cgit