fix more

coq-community · Nov 26, 2024 · d4b1fcc · d4b1fcc
1 parent ab04edb
commit d4b1fcc
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git a/theories/Structures/CoMonadLaws.v b/theories/Structures/CoMonadLaws.v
@@ -10,7 +10,7 @@ Section CoMonadLaws.
   Variable m : Type -> Type.
   Variable C : CoMonad m.
 
-  Class CoMonadLaws : Type :=
+  Class CoMonadLaws :=
     {
       extend_extract: forall (A B:Type),
         extend (B:=A) extract = id ;

diff --git a/theories/Structures/Foldable.v b/theories/Structures/Foldable.v
@@ -24,7 +24,7 @@ Section foldable.
 
   Variable Add : A -> T -> T -> Prop.
 
-  Class FoldableOk : Type :=
+  Class FoldableOk :=
   { fold_ind : forall m (M : Monoid m) (ML : MonoidLaws M) (P : m -> Prop) f u,
                  P (monoid_unit M) ->
                  (forall x y z,

diff --git a/theories/Structures/MonadLaws.v b/theories/Structures/MonadLaws.v
@@ -39,7 +39,7 @@ Section MonadLaws.
   Section with_state.
     Context {S : Type}.
 
-    Class MonadStateLaws  (MS : MonadState S m) : Type :=
+    Class MonadStateLaws  (MS : MonadState S m) :=
     { get_put : bind get put = ret tt :> m unit
     ; put_get : forall x : S,
         bind (put x) (fun _ => get) = bind (put x) (fun _ => ret x) :> m S
@@ -51,7 +51,7 @@ Section MonadLaws.
         bind get (fun _ => aM) = aM
     }.
 
-    Class MonadReaderLaws (MR : MonadReader S m) : Type :=
+    Class MonadReaderLaws (MR : MonadReader S m) :=
     { ask_local : forall f : S -> S,
         local f ask = bind ask (fun x => ret (f x))
     ; local_bind : forall {A B} (aM : m A) (f : S -> S) (g : A -> m B),
@@ -64,7 +64,7 @@ Section MonadLaws.
 
   End with_state.
 
-  Class MonadZeroLaws (MZ : MonadZero m) : Type :=
+  Class MonadZeroLaws (MZ : MonadZero m) :=
   { bind_zero : forall {A B} (f : A -> m B),
       bind mzero f = mzero
   }.