Commit 23f7fac4 authored by Ralf Jung's avatar Ralf Jung

bind types to scopes as early as possible, to functions get their arguments set appropriately

parent 492609d6
...@@ -15,6 +15,10 @@ Local Transparent uPred_holds. ...@@ -15,6 +15,10 @@ Local Transparent uPred_holds.
Add Printing Constructor uPred. Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3. Instance: Params (@uPred_holds) 3.
Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _.
Section cofe. Section cofe.
Context {M : cmraT}. Context {M : cmraT}.
Instance uPred_equiv : Equiv (uPred M) := λ P Q, x n, 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 := ...@@ -185,10 +189,6 @@ Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
{| uPred_holds n x := {n} a |}. {| uPred_holds n x := {n} a |}.
Solve Obligations with naive_solver eauto 2 using cmra_validN_le. 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 "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
Notation "(⊑)" := uPred_entails (only parsing) : C_scope. Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
Notation "■ φ" := (uPred_const φ%C%type) Notation "■ φ" := (uPred_const φ%C%type)
......
...@@ -49,6 +49,9 @@ Inductive val := ...@@ -49,6 +49,9 @@ Inductive val :=
| InjRV (v : val) | InjRV (v : val)
| LocV (l : loc). | LocV (l : loc).
Delimit Scope lang_scope with L.
Bind Scope lang_scope with expr val.
Fixpoint of_val (v : val) : expr := Fixpoint of_val (v : val) : expr :=
match v with match v with
| RecV f x e => Rec f x e | RecV f x e => Rec f x e
......
Require Export heap_lang.derived. Require Export heap_lang.derived.
Delimit Scope lang_scope with L.
Bind Scope lang_scope with expr val.
(* What about Arguments for hoare triples?. *) (* What about Arguments for hoare triples?. *)
Arguments wp {_ _} _ _%L _. Arguments wp {_ _} _ _%L _.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment