diff options
-rw-r--r-- | backend/Stackingproof.v | 1 | ||||
-rw-r--r-- | kvx/Stacklayout.v | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 1ede0194..49d2956e 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -139,6 +139,7 @@ Qed. (** * Memory assertions used to describe the contents of stack frames *) Local Opaque Z.add Z.mul Z.divide. +Local Hint Immediate perm_F_any : core. (** Accessing the stack frame using [load_stack] and [store_stack]. *) diff --git a/kvx/Stacklayout.v b/kvx/Stacklayout.v index 46202e03..740c0cf2 100644 --- a/kvx/Stacklayout.v +++ b/kvx/Stacklayout.v @@ -62,7 +62,7 @@ Lemma frame_env_separated: ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe)) ** P. Proof. -Local Opaque Z.add Z.mul sepconj range. +Local Opaque Z.add Z.mul sepconj range'. intros; simpl. set (w := if Archi.ptr64 then 8 else 4). set (olink := align (4 * b.(bound_outgoing)) w). |