Commit 0ca7041d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'ralf/scopes' into 'master'

Better %I scope handling

See merge request iris/iris!674
parents d502baa8 b600a5bb
......@@ -115,7 +115,7 @@ Record uPred (M : ucmra) : Type := UPred {
this way. *)
Local Coercion uPred_holds : uPred >-> Funclass.
Bind Scope bi_scope with uPred.
Global Arguments uPred_holds {_} _%I _ _ : simpl never.
Global Arguments uPred_holds {_} _ _ _ : simpl never.
Add Printing Constructor uPred.
Global Instance: Params (@uPred_holds) 3 := {}.
......
......@@ -182,6 +182,7 @@ Structure bi := Bi {
bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
bi_forall bi_exist bi_sep bi_persistently bi_later;
}.
Bind Scope bi_scope with bi_car.
Coercion bi_ofeO (PROP : bi) : ofe := Ofe PROP (bi_ofe_mixin PROP).
Canonical Structure bi_ofeO.
......@@ -204,18 +205,18 @@ Global Instance: Params (@bi_later) 1 := {}.
Global Arguments bi_car : simpl never.
Global Arguments bi_dist : simpl never.
Global Arguments bi_equiv : simpl never.
Global Arguments bi_entails {PROP} _%I _%I : simpl never, rename.
Global Arguments bi_entails {PROP} _ _ : simpl never, rename.
Global Arguments bi_emp {PROP} : simpl never, rename.
Global Arguments bi_pure {PROP} _%stdpp : simpl never, rename.
Global Arguments bi_and {PROP} _%I _%I : simpl never, rename.
Global Arguments bi_or {PROP} _%I _%I : simpl never, rename.
Global Arguments bi_impl {PROP} _%I _%I : simpl never, rename.
Global Arguments bi_and {PROP} _ _ : simpl never, rename.
Global Arguments bi_or {PROP} _ _ : simpl never, rename.
Global Arguments bi_impl {PROP} _ _ : simpl never, rename.
Global Arguments bi_forall {PROP _} _%I : simpl never, rename.
Global Arguments bi_exist {PROP _} _%I : simpl never, rename.
Global Arguments bi_sep {PROP} _%I _%I : simpl never, rename.
Global Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
Global Arguments bi_persistently {PROP} _%I : simpl never, rename.
Global Arguments bi_later {PROP} _%I : simpl never, rename.
Global Arguments bi_sep {PROP} _ _ : simpl never, rename.
Global Arguments bi_wand {PROP} _ _ : simpl never, rename.
Global Arguments bi_persistently {PROP} _ : simpl never, rename.
Global Arguments bi_later {PROP} _ : simpl never, rename.
Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
......
......@@ -7,3 +7,10 @@ Proof. apply _. Qed.
Lemma test_impl_persistent_2 `{!BiPlainly PROP} :
Persistent (PROP:=PROP) (True True True).
Proof. apply _. Qed.
(* Test that the right scopes are used. *)
Lemma test_bi_scope {PROP : bi} : True.
Proof.
(* [<affine> True] is implicitly in %I scope. *)
pose proof (bi.wand_iff_refl (PROP:=PROP) (<affine> True)).
Abort.
Supports Markdown
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