warning, bump analysis version

coq-monae.opam

@@ -24,7 +24,7 @@ depends: [
   "coq-mathcomp-algebra" { (>= "2.3.0") | (= "dev")  }
   "coq-mathcomp-solvable" { (>= "2.3.0") | (= "dev")  }
   "coq-mathcomp-field" { (>= "2.3.0") | (= "dev")  }
-  "coq-mathcomp-analysis" { (>= "1.7.0")}
+  "coq-mathcomp-analysis" { (>= "1.8.0")}
   "coq-infotheo" { >= "0.7.6"}
   "coq-paramcoq" { >= "1.1.3" & < "1.2~" }
   "coq-hierarchy-builder" { >= "1.7.0" }

impredicative_set/ihierarchy.v

@@ -776,7 +776,7 @@ HB.structure Definition MonadAlt := {M of isMonadAlt M & }.
 Notation "a [~] b" := (@alt _ _ a b). (* infix notation *)
 
 HB.mixin Record isMonadAltCI (M : UU0 -> UU0) of MonadAlt M := {
-  altmm : forall A : UU0, idempotent (@alt M A) ;
+  altmm : forall A : UU0, idempotent_op (@alt M A) ;
   altC : forall A : UU0, commutative (@alt M A) }.
 
 #[short(type=altCIMonad)]

meta.yml

@@ -72,7 +72,7 @@ dependencies:
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "1.7.0")}'
+    version: '{ (>= "1.8.0")}'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
 - opam:

theories/core/hierarchy.v

@@ -795,7 +795,7 @@ HB.structure Definition MonadAlt := {M of isMonadAlt M & }.
 Notation "a [~] b" := (@alt _ _ a b). (* infix notation *)
 
 HB.mixin Record isMonadAltCI (M : UU0 -> UU0) of MonadAlt M := {
-  altmm : forall A : UU0, idempotent (@alt M A) ;
+  altmm : forall A : UU0, idempotent_op (@alt M A) ;
   altC : forall A : UU0, commutative (@alt M A) }.
 
 #[short(type=altCIMonad)]
@@ -1253,7 +1253,7 @@ HB.mixin Record isMonadConvex {R : realType} (M : UU0 -> UU0) of Monad M := {
   (* skewed commutativity *)
   choiceC : forall (T : UU0) p (a b : M T),
     choice p _ a b = choice (p.~%:pr) _ b a ;
-  choicemm : forall (T : UU0) p, idempotent (@choice p T) ;
+  choicemm : forall (T : UU0) p, idempotent_op (@choice p T) ;
   (* quasi associativity *)
   choiceA : forall (T : UU0) (p q r s : {prob R}) (a b c : M T),
     choice p _ a (choice q _ b c) = choice [s_of p, q] _ (choice [r_of p, q] _ a b) c }.

theories/models/proba_monad_model.v

@@ -58,7 +58,7 @@ Proof. by move=> ? ?; exact: conv1. Qed.
 Let choiceC (T : UU0) : forall p (a b : acto T), choice p _ a b = choice ((Prob.p p).~ %:pr) _ b a.
 Proof. by move=> ? ?; exact: convC. Qed.
 
-Let choicemm : forall (T : Type) p, idempotent (@choice p T).
+Let choicemm : forall (T : Type) p, idempotent_op (@choice p T).
 Proof. by move=> ? ? ?; exact: convmm. Qed.
 
 Let choiceA : forall (T : Type) (p q r s : {prob R}) (a b c : acto T),