diff --git a/stdpp/base.v b/stdpp/base.v index 9b98d72881ef6e76bc820befefe57643dea40511..f9daa20054439c6bfc59142581733fd1d275d3dd 100644 --- a/stdpp/base.v +++ b/stdpp/base.v @@ -1144,27 +1144,27 @@ class with the monad laws). *) Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A. Global Arguments mret {_ _ _} _ : assert. Global Instance: Params (@mret) 3 := {}. -Global Hint Mode MRet ! : typeclass_instances. +Global Hint Mode MRet + : typeclass_instances. Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B. Global Arguments mbind {_ _ _ _} _ !_ / : assert. Global Instance: Params (@mbind) 4 := {}. -Global Hint Mode MBind ! : typeclass_instances. +Global Hint Mode MBind + : typeclass_instances. Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A. Global Arguments mjoin {_ _ _} !_ / : assert. Global Instance: Params (@mjoin) 3 := {}. -Global Hint Mode MJoin ! : typeclass_instances. +Global Hint Mode MJoin + : typeclass_instances. Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B. Global Arguments fmap {_ _ _ _} _ !_ / : assert. Global Instance: Params (@fmap) 4 := {}. -Global Hint Mode FMap ! : typeclass_instances. +Global Hint Mode FMap + : typeclass_instances. Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B. Global Arguments omap {_ _ _ _} _ !_ / : assert. Global Instance: Params (@omap) 4 := {}. -Global Hint Mode OMap ! : typeclass_instances. +Global Hint Mode OMap + : typeclass_instances. Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope. Notation "( m ≫=.)" := (λ f, mbind f m) (only parsing) : stdpp_scope.