diff options
Diffstat (limited to 'backend/Stackingproof.v')
| -rw-r--r-- | backend/Stackingproof.v | 1 |
1 files changed, 1 insertions, 0 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]. *) |