avoid name clash

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -130,6 +130,9 @@
 - in `charge.v`:
   + `induced` -> `induced_charge`
 
+- in `boolp.v`:
+  + `notP` -> `not_notP`
+
 ### Generalized
 
 - in `lebesgue_integral_under.v`:

classical/boolp.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 (* -------------------------------------------------------------------- *)
 (* Copyright (c) - 2015--2016 - IMDEA Software Institute                *)
 (* Copyright (c) - 2015--2018 - Inria                                   *)
@@ -683,10 +683,12 @@ by rewrite 2!negb_and -3!asbool_neg => /or3_asboolP.
 by rewrite 3!asbool_neg -2!negb_and => /and3_asboolP.
 Qed.
 
-Lemma notP (P : Prop) : ~ ~ P <-> P.
+Lemma not_notP (P : Prop) : ~ ~ P <-> P.
 Proof. by split => [|p]; [exact: contrapT|exact]. Qed.
+#[deprecated(since="mathcomp-analysis 1.15.0", note="Renamed to `not_notP`. Warning: a different `notP` is also provided by `contra.v`.")]
+Notation notP := not_notP (only parsing).
 
-Lemma notE (P : Prop) : (~ ~ P) = P. Proof. by rewrite propeqE notP. Qed.
+Lemma notE (P : Prop) : (~ ~ P) = P. Proof. by rewrite propeqE not_notP. Qed.
 
 Lemma not_orE (P Q : Prop) : (~ (P \/ Q)) = (~ P /\ ~ Q).
 Proof. by rewrite -[_ /\ _]notE not_andE 2!notE. Qed.

theories/normedtype_theory/normed_module.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint.
 From mathcomp Require Import archimedean rat interval zmodp vector.
@@ -2299,7 +2299,7 @@ suff [p_idx [pUq Up]] : exists p_idx,
     by move/set_mem : pUq; exact: bigcup_ointsub_sub.
   exists (g p_idx).
   - rewrite /= => q' Uq' q'p.
-    apply/notP => /eqP/set0P[s [ps ts]].
+    apply/not_notP => /eqP/set0P[s [ps ts]].
     suff : ratr q' \in bigcup_ointsub U q by move/Up; rewrite leqNgt q'p.
     rewrite (@nondisjoint_bigcup_ointsub _ _ _ (g p_idx))//.
     rewrite (@nondisjoint_bigcup_ointsub _ _ _ q') ?bigcup_ointsubxx//.

theories/sequences.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint.
 From mathcomp Require Import interval interval_inference archimedean.
@@ -2899,7 +2899,7 @@ have akN1A : a_ k.-1 \in A.
     contra: aiB => ->.
     rewrite /a_ !mul0r addr0; apply/negP => /set_mem/(ABlt _ _ aA).
     by rewrite ltxx.
-  apply/mem_set/boolp.notP => abs.
+  apply/mem_set/not_notP => abs.
   have {}abs : a_ i.-1 \in B.
     by move/seteqP : ABT => [_ /(_ (a_ i.-1) Logic.I)] [//|/mem_set].
   have iN : (i.-1 < N.+1)%N by rewrite prednK ?lt0n// ltnW.
@@ -3253,7 +3253,7 @@ have majball g x : F g -> (ball x0 r%:num) x -> `|g (x - x0)| <= n%:R + n%:R.
   move: (linearB (pack_linear Lg)) => /= -> Ballx.
   apply/(le_trans (ler_normB _ _))/lerD; first exact: majballi.
   by apply: majballi => //; exact/ball_center.
-have ballprop : ball x0 r%:num (2^-1 * (r%:num / `|y|) *: y  + x0).
+have ballprop : ball x0 r%:num (2^-1 * (r%:num / `|y|) *: y + x0).
   rewrite -ball_normE /ball_ /= opprD addrC subrK normrN normrZ.
   rewrite 2!normrM 2!normfV normr_id !mulrA divfK ?normr_eq0//.
   by rewrite !gtr0_norm// gtr_pMl// invf_lt1// ltr1n.