Skip to content
Snippets Groups Projects
Verified Commit f33e1e72 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Avoid double instance for fupd_proper

parent 2b579aab
No related tags found
No related merge requests found
...@@ -13,7 +13,7 @@ Notation "P ==∗ Q" := (P ⊢ |==> Q) (only parsing) : stdpp_scope. ...@@ -13,7 +13,7 @@ Notation "P ==∗ Q" := (P ⊢ |==> Q) (only parsing) : stdpp_scope.
Notation "P ==∗ Q" := (P -∗ |==> Q)%I : bi_scope. Notation "P ==∗ Q" := (P -∗ |==> Q)%I : bi_scope.
Class FUpd (PROP : Type) : Type := fupd : coPset coPset PROP PROP. Class FUpd (PROP : Type) : Type := fupd : coPset coPset PROP PROP.
Instance: Params (@fupd) 4 := {}. Instance: Params (@fupd) 2 := {}.
Hint Mode FUpd ! : typeclass_instances. Hint Mode FUpd ! : typeclass_instances.
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope. Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
...@@ -213,11 +213,9 @@ Section fupd_derived. ...@@ -213,11 +213,9 @@ Section fupd_derived.
Context `{BiFUpd PROP}. Context `{BiFUpd PROP}.
Implicit Types P Q R : PROP. Implicit Types P Q R : PROP.
Global Instance fupd_proper' : Global Instance fupd_proper :
Proper (() ==> () ==> () ==> ()) (fupd (PROP:=PROP)). Proper (() ==> () ==> () ==> ()) (fupd (PROP:=PROP)).
Proof. solve_proper_prepare. exact: ne_proper. Qed. Proof. solve_proper_prepare. exact: ne_proper. Qed.
Global Instance fupd_proper E1 E2 :
Proper (() ==> ()) (fupd (PROP:=PROP) E1 E2). Proof. solve_proper. Qed.
(** FUpd derived rules *) (** FUpd derived rules *)
Global Instance fupd_mono' E1 E2 : Proper (() ==> ()) (fupd (PROP:=PROP) E1 E2). Global Instance fupd_mono' E1 E2 : Proper (() ==> ()) (fupd (PROP:=PROP) E1 E2).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment