diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v index 6dbb677f2213370298615c3f5885570fd3fb4db9..3a38ffa34c1de63c409f3b2c1055f2865e745abf 100644 --- a/theories/algebra/agree.v +++ b/theories/algebra/agree.v @@ -193,7 +193,7 @@ Section list_theory. Context `(R' : relation B) (f : A → B) {Hf: Proper (R ==> R') f}. Collection Hyps := Type Hf. Local Set Default Proof Using "Hyps". - + Global Instance list_setincl_fmap : Proper (list_setincl R ==> list_setincl R') (fmap f). Proof using Hf. @@ -201,7 +201,7 @@ Section list_theory. destruct (Hab _ Ha) as (b & Hb & HR). exists (f b). split; first eapply elem_of_list_fmap; eauto. Qed. - + Global Instance list_setequiv_fmap : Proper (list_setequiv R ==> list_setequiv R') (fmap f). Proof using Hf. intros ?? [??]. split; apply list_setincl_fmap; done. Qed. @@ -213,9 +213,7 @@ Section list_theory. intros (a & -> & Ha)%elem_of_list_fmap (b & -> & Hb)%elem_of_list_fmap. apply Hf. exact: Hl. Qed. - End fmap. - End list_theory. Section agree. @@ -408,6 +406,7 @@ Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊢ (x ≡ y : uPred M). Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed. End agree. +Instance: Params (@to_agree) 1. Arguments agreeC : clear implicits. Arguments agreeR : clear implicits. diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v index a2a508433c76402fae42340957a41d29cfcbd5a7..4fb69bd328e32a15c7f1b880cc146c4cb1d99248 100644 --- a/theories/algebra/csum.v +++ b/theories/algebra/csum.v @@ -10,13 +10,17 @@ Local Arguments cmra_validN _ _ !_ /. Local Arguments cmra_valid _ !_ /. Inductive csum (A B : Type) := -| Cinl : A → csum A B -| Cinr : B → csum A B -| CsumBot : csum A B. + | Cinl : A → csum A B + | Cinr : B → csum A B + | CsumBot : csum A B. Arguments Cinl {_ _} _. Arguments Cinr {_ _} _. Arguments CsumBot {_ _}. +Instance: Params (@Cinl) 2. +Instance: Params (@Cinr) 2. +Instance: Params (@CsumBot) 2. + Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x, match x with Cinl a => Some a | _ => None end. Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x, diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v index ca8757a07cfae769bd8e771d9c1c3c1fd3e10a81..70b6e3a44b6fb0674284a29e449cabcdbc035425 100644 --- a/theories/algebra/excl.v +++ b/theories/algebra/excl.v @@ -10,6 +10,9 @@ Inductive excl (A : Type) := Arguments Excl {_} _. Arguments ExclBot {_}. +Instance: Params (@Excl) 1. +Instance: Params (@ExclBot) 1. + Notation excl' A := (option (excl A)). Notation Excl' x := (Some (Excl x)). Notation ExclBot' := (Some ExclBot). diff --git a/theories/prelude/base.v b/theories/prelude/base.v index ccd30423724ba4dc656018139d82d2dc46473776..65233ddfe3a3be343c6437f242577bc10dbd6936 100644 --- a/theories/prelude/base.v +++ b/theories/prelude/base.v @@ -422,6 +422,8 @@ Notation "p .1" := (fst p) (at level 10, format "p .1"). Notation "p .2" := (snd p) (at level 10, format "p .2"). Instance: Params (@pair) 2. +Instance: Params (@fst) 2. +Instance: Params (@snd) 2. Notation curry := prod_curry. Notation uncurry := prod_uncurry.