diff --git a/algebra/upred.v b/algebra/upred.v index 3aa4b20bf4e3277c4253343c488aeb52e56a146f..c3279bd976c21872f4f5a9e9a05ba334f657e237 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -15,6 +15,10 @@ Local Transparent uPred_holds. Add Printing Constructor uPred. Instance: Params (@uPred_holds) 3. +Delimit Scope uPred_scope with I. +Bind Scope uPred_scope with uPred. +Arguments uPred_holds {_} _%I _ _. + Section cofe. Context {M : cmraT}. Instance uPred_equiv : Equiv (uPred M) := λ P Q, ∀ x n, @@ -185,10 +189,6 @@ Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M := {| uPred_holds n x := ✓{n} a |}. Solve Obligations with naive_solver eauto 2 using cmra_validN_le. -Delimit Scope uPred_scope with I. -Bind Scope uPred_scope with uPred. -Arguments uPred_holds {_} _%I _ _. -Arguments uPred_entails _ _%I _%I. Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope. Notation "(⊑)" := uPred_entails (only parsing) : C_scope. Notation "■ φ" := (uPred_const φ%C%type) diff --git a/heap_lang/heap_lang.v b/heap_lang/heap_lang.v index eba60945618504d05b209b10771eb43c9f16d7db..be2503d780ad35a416a428a99ebe81745cabbf9b 100644 --- a/heap_lang/heap_lang.v +++ b/heap_lang/heap_lang.v @@ -49,6 +49,9 @@ Inductive val := | InjRV (v : val) | LocV (l : loc). +Delimit Scope lang_scope with L. +Bind Scope lang_scope with expr val. + Fixpoint of_val (v : val) : expr := match v with | RecV f x e => Rec f x e diff --git a/heap_lang/notation.v b/heap_lang/notation.v index fb7efc5da7459b83ee18e8513c2827bf67c22be5..fe4affa41bcc41cb728753ef38f8a45051cfbfc2 100644 --- a/heap_lang/notation.v +++ b/heap_lang/notation.v @@ -1,8 +1,5 @@ Require Export heap_lang.derived. -Delimit Scope lang_scope with L. -Bind Scope lang_scope with expr val. - (* What about Arguments for hoare triples?. *) Arguments wp {_ _} _ _%L _.