diff options
Diffstat (limited to 'common/Separation.v')
| -rw-r--r-- | common/Separation.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/common/Separation.v b/common/Separation.v index f41d94c3..2ba6e77b 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -54,6 +54,7 @@ Record massert : Type := { m_valid: forall m b ofs, m_pred m -> m_footprint b ofs -> Mem.valid_block m b }. +Declare Scope sep_scope. Notation "m |= p" := (m_pred p m) (at level 74, no associativity) : sep_scope. (** Implication and logical equivalence between memory predicates *) |