diff options
Diffstat (limited to 'common/Memory.v')
| -rw-r--r-- | common/Memory.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/common/Memory.v b/common/Memory.v index 641a9243..b16a98b6 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -4500,7 +4500,7 @@ Notation mem := Mem.mem. Global Opaque Mem.alloc Mem.free Mem.store Mem.load Mem.storebytes Mem.loadbytes. -Hint Resolve +Global Hint Resolve Mem.valid_not_valid_diff Mem.perm_implies Mem.perm_cur |