upd

Author: affeldt-aist

rocq-mathcomp-analysis.opam

@@ -19,7 +19,6 @@ depends: [
   "rocq-mathcomp-solvable"
   "rocq-mathcomp-field"
   "rocq-mathcomp-bigenough" { (>= "1.0.0") }
-  "rocq-mathcomp-algebra-tactics" { (>= "1.2.7") }
   "rocq-navi" {= "0.4.1" & with-doc}
 ]
 

theories/probability_theory/normal_distribution.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval.
-From mathcomp Require Import archimedean finmap interval_inference ring.
+From mathcomp Require Import archimedean finmap interval_inference ring_tactic.
 From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
 From mathcomp Require Import reals ereal topology normedtype sequences derive.
 From mathcomp Require Import measure exp trigo numfun realfun.