fix

math-comp · Oct 27, 2024 · 4d3f8a7 · 4d3f8a7
1 parent 8a266dc
commit 4d3f8a7
Showing 1 changed file with 0 additions and 5 deletions.
diff --git a/theories/probability.v b/theories/probability.v
@@ -112,9 +112,6 @@ Proof. by move=> mf f0; rewrite integral_pushforward. Qed.
 
 End transfer_probability.
 
-Require Import kernel.
-
-
 (* a pker that takes a superfluous arg *)
 Section pker_curry.
 Context d {T : measurableType d} {R : realType}
@@ -190,8 +187,6 @@ Qed.
 HB.instance Definition _ :=
   @Measure_isProbability.Build _ _ _ bind bindT.
 
-Check bind : probability T' R.
-
 End giry_def.
 
 Section giry_prop.