From 89211943657bcdb5ee2f2f8bbda26ac379f59493 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 7 Nov 2023 10:33:15 +0100
Subject: [PATCH] Adapt to https://github.com/math-comp/math-comp/pull/1110

---
 theories/numbers/ssete7.v  | 2 +-
 theories/ordinals/sset15.v | 2 +-
 theories/sets/sset1.v      | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/numbers/ssete7.v b/theories/numbers/ssete7.v
index 78069ff..5a48d9a 100644
--- a/theories/numbers/ssete7.v
+++ b/theories/numbers/ssete7.v
@@ -1309,7 +1309,7 @@ rewrite !muln1 mulnDl mulnC addnCA; congr (_ + _).
 Qed.
 
 
-Lemma F22 n: \sum_(i<n) i `! * i = n `! .-1.
+Lemma F22 n: \sum_(i<n) i `! * i = (n `! ).-1.
 Proof.
 elim: n; first by rewrite big_ord0.
 move => n Hrec;rewrite  big_ord_recr /=  Hrec {Hrec}.
diff --git a/theories/ordinals/sset15.v b/theories/ordinals/sset15.v
index e883f08..10df3f5 100644
--- a/theories/ordinals/sset15.v
+++ b/theories/ordinals/sset15.v
@@ -4731,7 +4731,7 @@ move: sc => [ix sx].
 have pf':~ (exists a : Set, cpow_less_ec_prop \2c x a).
   by move => [a [px py]]; case: pf; exists a.
 move: (cpow_less_ec_pr6 ix le22 pf') => eq1.
-have pa: (\2c ^c \cf (\2c ^<c x)) <c \2c ^<c x.
+have pa: (\2c ^c (\cf (\2c ^<c x))) <c \2c ^<c x.
   have pb:= (cofinality_small ix).
   move: (aux _ (conj pb sx)) => [b [p1 p2 p3]].
   by rewrite eq1; apply: (clt_leT p3); apply: cpow_less_pr2.
diff --git a/theories/sets/sset1.v b/theories/sets/sset1.v
index 6ae1d94..3ab47c2 100644
--- a/theories/sets/sset1.v
+++ b/theories/sets/sset1.v
@@ -111,7 +111,7 @@ Axiom IM_P :  forall (x : Set) (f : x -> Set) (y : Set),
 
 Axiom p_or_not_p: forall P:Prop,  P \/ ~ P.
 
-Lemma ixm (P: Prop): P + ~P.
+Lemma ixm (P: Prop): P + (~P).
 Proof.
 apply: (chooseT (fun _ => True)).
 by case: (p_or_not_p P) => H;constructor; [ left | right ].
@@ -1030,7 +1030,7 @@ Definition powerset (x : Set) :=
  IM (fun p : x -> C2 =>
     Zo x (fun y : Set => forall hyp : inc y x, Ro (p (Bo hyp)) = C0)).
 
-Notation "\Po E" :=   (powerset E) (at level 40).  
+Notation "\Po E" :=   (powerset E) (at level 30).
 
 Lemma setP_i y x : sub y x -> inc y (\Po x). 
 Proof.