diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam
index a449b7aec..5c038a008 100644
--- a/coq-mathcomp-analysis.opam
+++ b/coq-mathcomp-analysis.opam
@@ -22,7 +22,8 @@ depends: [
   "coq-mathcomp-solvable" { (>= "2.0.0") | (= "dev") }
   "coq-mathcomp-field"
   "coq-mathcomp-bigenough" { (>= "1.0.0") }
-  "coq-mathcomp-algebra-tactics" { (>= "1.1.1") }
+  "coq-mathcomp-algebra-tactics" { (>= "1.2.0") }
+  "coq-mathcomp-zify" { (>= "1.4.0") }
 ]
 
 tags: [
diff --git a/theories/lang_syntax.v b/theories/lang_syntax.v
index ac3c32e4f..5c1542ee1 100644
--- a/theories/lang_syntax.v
+++ b/theories/lang_syntax.v
@@ -1,8 +1,8 @@
 Require Import String.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
-From mathcomp.classical Require Import functions cardinality fsbigop.
+From mathcomp Require Import mathcomp_extra boolp classical_sets.
+From mathcomp Require Import functions cardinality fsbigop.
 Require Import signed reals ereal topology normedtype sequences esum measure.
 Require Import lebesgue_measure numfun lebesgue_integral kernel prob_lang.
 Require Import lang_syntax_util.
@@ -89,7 +89,7 @@ Proof. done. Qed.
 Let mswap_sigma_additive x : semi_sigma_additive (mswap x).
 Proof. exact: measure_semi_sigma_additive. Qed.
 
-HB.instance Definition _ x := isMeasure.Build _ R _
+HB.instance Definition _ x := isMeasure.Build _ _ R
   (mswap x) (mswap0 x) (mswap_ge0 x) (@mswap_sigma_additive x).
 
 Definition mkswap : _ -> {measure set Z -> \bar R} :=
@@ -185,24 +185,22 @@ Let T0 z : (T' z) set0 = 0. Proof. by []. Qed.
 Let T_ge0 z x : 0 <= (T' z) x. Proof. by []. Qed.
 Let T_semi_sigma_additive z : semi_sigma_additive (T' z).
 Proof. exact: measure_semi_sigma_additive. Qed.
-HB.instance Definition _ z := @isMeasure.Build _ R X (T' z) (T0 z) (T_ge0 z)
+HB.instance Definition _ z := @isMeasure.Build _ X R (T' z) (T0 z) (T_ge0 z)
   (@T_semi_sigma_additive z).
 
 Let sfinT z : sfinite_measure (T' z). Proof. exact: sfinite_kernel_measure. Qed.
-HB.instance Definition _ z := @Measure_isSFinite_subdef.Build _ X R
-  (T' z) (sfinT z).
+HB.instance Definition _ z := @isSFinite.Build _ X R (T' z) (sfinT z).
 
 Definition U' z : set Y -> \bar R := u z.
 Let U0 z : (U' z) set0 = 0. Proof. by []. Qed.
 Let U_ge0 z x : 0 <= (U' z) x. Proof. by []. Qed.
 Let U_semi_sigma_additive z : semi_sigma_additive (U' z).
 Proof. exact: measure_semi_sigma_additive. Qed.
-HB.instance Definition _ z := @isMeasure.Build _ R Y (U' z) (U0 z) (U_ge0 z)
+HB.instance Definition _ z := @isMeasure.Build _ Y R (U' z) (U0 z) (U_ge0 z)
   (@U_semi_sigma_additive z).
 
 Let sfinU z : sfinite_measure (U' z). Proof. exact: sfinite_kernel_measure. Qed.
-HB.instance Definition _ z := @Measure_isSFinite_subdef.Build _ Y R
-  (U' z) (sfinU z).
+HB.instance Definition _ z := @isSFinite.Build _ Y R (U' z) (sfinU z).
 
 Lemma letin'C z A : measurable A ->
   letin' t
@@ -271,7 +269,7 @@ Inductive typ :=
 | Pair : typ -> typ -> typ
 | Prob : typ -> typ.
 
-Canonical stype_eqType := Equality.Pack (@gen_eqMixin typ).
+HB.instance Definition _ := gen_eqMixin typ.
 
 Fixpoint measurable_of_typ (t : typ) : {d & measurableType d} :=
   match t with
diff --git a/theories/lang_syntax_examples.v b/theories/lang_syntax_examples.v
index 8a365773e..4be13e9c5 100644
--- a/theories/lang_syntax_examples.v
+++ b/theories/lang_syntax_examples.v
@@ -59,7 +59,7 @@ Lemma letin'_sample_bernoulli d d' (T : measurableType d)
 Proof.
 rewrite letin'E/=.
 rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=.
-by rewrite !ge0_integral_mscale//= !integral_dirac//= indicT 2!mul1e.
+by rewrite !ge0_integral_mscale//= !integral_dirac//= !diracT 2!mul1e.
 Qed.
 
 Section letin'_return.
@@ -81,7 +81,7 @@ Lemma letin'_retk (f : X -> Y) (mf : measurable_fun setT f)
     (k : R.-sfker Y * X ~> Z) x U :
   measurable U -> letin' (ret mf) k x U = k (f x, x) U.
 Proof.
-move=> mU; rewrite letin'E retE integral_dirac ?indicT ?mul1e//.
+move=> mU; rewrite letin'E retE integral_dirac ?diracT ?mul1e//.
 exact: (measurableT_comp (measurable_kernel k _ mU)).
 Qed.
 
@@ -209,38 +209,38 @@ Definition sample_pair_syntax : exp _ [::] _ :=
 Lemma exec_sample_pair0 (A : set (bool * bool)) :
   @execP R [::] _ sample_pair_syntax0 tt A =
   ((1 / 2)%:E *
-   ((1 / 3)%:E * ((true, true) \in A)%:R%:E +
-    (1 - 1 / 3)%:E * ((true, false) \in A)%:R%:E) +
+   ((1 / 3)%:E * \d_(true, true) A +
+    (1 - 1 / 3)%:E * \d_(true, false) A) +
    (1 - 1 / 2)%:E *
-   ((1 / 3)%:E * ((false, true) \in A)%:R%:E +
-    (1 - 1 / 3)%:E * ((false, false) \in A)%:R%:E))%E.
+   ((1 / 3)%:E * \d_(false, true) A +
+    (1 - 1 / 3)%:E * \d_(false, false) A))%E.
 Proof.
 rewrite !execP_letin !execP_sample !execD_bernoulli execP_return /=.
 rewrite execD_pair !exp_var'E (execD_var_erefl "x") (execD_var_erefl "y") /=.
 rewrite letin'E integral_measure_add//= !ge0_integral_mscale//= /onem.
-rewrite !integral_dirac//= !indicE !in_setT/= !mul1e.
+rewrite !integral_dirac//= !diracT !mul1e.
 rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem.
-by rewrite !integral_dirac//= !indicE !in_setT/= !mul1e !diracE.
+by rewrite !integral_dirac//= !diracT !mul1e.
 Qed.
 
 Lemma exec_sample_pair0_TandT :
   @execP R [::] _ sample_pair_syntax0 tt [set (true, true)] = (1 / 6)%:E.
 Proof.
-rewrite exec_sample_pair0 mem_set//; do 3 rewrite memNset//=.
+rewrite exec_sample_pair0 !diracE mem_set//; do 3 rewrite memNset//=.
 by rewrite /= !mule0 mule1 !add0e mule0 adde0; congr (_%:E); lra.
 Qed.
 
 Lemma exec_sample_pair0_TandF :
   @execP R [::] _ sample_pair_syntax0 tt [set (true, false)] = (1 / 3)%:E.
 Proof.
-rewrite exec_sample_pair0 memNset// mem_set//; do 2 rewrite memNset//.
+rewrite exec_sample_pair0 !diracE memNset// mem_set//; do 2 rewrite memNset//.
 by rewrite /= !mule0 mule1 !add0e mule0 adde0; congr (_%:E); lra.
 Qed.
 
 Lemma exec_sample_pair0_TandT' :
   @execP R [::] _ sample_pair_syntax0 tt [set p | p.1 && p.2] = (1 / 6)%:E.
 Proof.
-rewrite exec_sample_pair0 mem_set//; do 3 rewrite memNset//=.
+rewrite exec_sample_pair0 !diracE mem_set//; do 3 rewrite memNset//=.
 by rewrite /= !mule0 mule1 !add0e mule0 adde0; congr (_%:E); lra.
 Qed.
 
@@ -248,9 +248,9 @@ Lemma exec_sample_pair_TorT :
   (projT1 (execD sample_pair_syntax)) tt [set p | p.1 || p.2] = (2 / 3)%:E.
 Proof.
 rewrite execD_normalize_pt normalizeE/= exec_sample_pair0.
-do 4 rewrite mem_set//=.
+rewrite !diracE; do 4 rewrite mem_set//=.
 rewrite eqe ifF; last by apply/negbTE/negP => /orP[/eqP|//]; lra.
-rewrite exec_sample_pair0; do 3 rewrite mem_set//; rewrite memNset//=.
+rewrite exec_sample_pair0 !diracE; do 3 rewrite mem_set//; rewrite memNset//=.
 by rewrite !mule1; congr (_%:E); field.
 Qed.
 
@@ -260,18 +260,17 @@ Definition sample_and_syntax0 : @exp R _ [::] _ :=
    return #{"x"} && #{"y"}].
 
 Lemma exec_sample_and0 (A : set bool) :
-  @execP R [::] _ sample_and_syntax0 tt A =
-  ((1 / 6)%:E * (true \in A)%:R%:E +
-  (1 - 1 / 6)%:E * (false \in A)%:R%:E)%E.
+  @execP R [::] _ sample_and_syntax0 tt A = ((1 / 6)%:E * \d_true A +
+                                             (1 - 1 / 6)%:E * \d_false A)%E.
 Proof.
 rewrite !execP_letin !execP_sample !execD_bernoulli execP_return /=.
 rewrite (@execD_bin _ _ binop_and) !exp_var'E (execD_var_erefl "x") (execD_var_erefl "y") /=.
 rewrite letin'E integral_measure_add//= !ge0_integral_mscale//= /onem.
-rewrite !integral_dirac//= !indicE !in_setT/= !mul1e.
+rewrite !integral_dirac//= !diracT !mul1e.
 rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem.
-rewrite !integral_dirac//= !indicE !in_setT/= !mul1e !diracE.
+rewrite !integral_dirac//= !diracT !mul1e.
 rewrite muleDr// -addeA; congr (_ + _)%E.
-by rewrite !muleA; congr (_%:E); congr (_ * _); field.
+  by rewrite !muleA; congr (_%:E); congr (_ * _); field.
 rewrite -muleDl// !muleA -muleDl//.
 by congr (_%:E); congr (_ * _); field.
 Qed.
@@ -283,19 +282,18 @@ Definition sample_bernoulli_and3 : @exp R _ [::] _ :=
    return #{"x"} && #{"y"} && #{"z"}].
 
 Lemma exec_sample_bernoulli_and3 t U :
-  execP sample_bernoulli_and3 t U =
-  ((1 / 8)%:E * (true \in U)%:R%:E +
-  (1 - 1 / 8)%:E * (false \in U)%:R%:E)%E.
+  execP sample_bernoulli_and3 t U = ((1 / 8)%:E * \d_true U +
+                                     (1 - 1 / 8)%:E * \d_false U)%E.
 Proof.
 rewrite !execP_letin !execP_sample !execD_bernoulli execP_return /=.
 rewrite !(@execD_bin _ _ binop_and) !exp_var'E.
 rewrite (execD_var_erefl "x") (execD_var_erefl "y") (execD_var_erefl "z") /=.
 rewrite letin'E integral_measure_add//= !ge0_integral_mscale//= /onem.
-rewrite !integral_dirac//= !indicE !in_setT/= !mul1e.
+rewrite !integral_dirac//= !diracT !mul1e.
 rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem.
-rewrite !integral_dirac//= !indicE !in_setT/= !mul1e.
+rewrite !integral_dirac//= !diracT !mul1e.
 rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem.
-rewrite !integral_dirac//= !indicE !in_setT/= !mul1e !diracE.
+rewrite !integral_dirac//= !diracT !mul1e.
 rewrite !muleDr// -!addeA.
 by congr (_ + _)%E; rewrite ?addeA !muleA -?muleDl//;
 congr (_ * _)%E; congr (_%:E); field.
@@ -307,25 +305,6 @@ Definition sample_add_syntax0 : @exp R _ [::] _ :=
    let "z" := Sample {exp_bernoulli (1 / 2)%:nng (p1S 1)} in
    return #{"x"} && #{"y"} && #{"z"}].
 
-Lemma exec_sample_bernoulli_and3 t U :
-  execP sample_bernoulli_and3 t U =
-  ((1 / 8)%:E * (true \in U)%:R%:E +
-  (1 - 1 / 8)%:E * (false \in U)%:R%:E)%E.
-Proof.
-rewrite !execP_letin !execP_sample !execD_bernoulli execP_return /=.
-rewrite !(@execD_bin _ _ binop_and) !exp_var'E.
-rewrite (execD_var_erefl "x") (execD_var_erefl "y") (execD_var_erefl "z") /=.
-rewrite letin'E integral_measure_add//= !ge0_integral_mscale//= /onem.
-rewrite !integral_dirac//= !indicE !in_setT/= !mul1e.
-rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem.
-rewrite !integral_dirac//= !indicE !in_setT/= !mul1e.
-rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem.
-rewrite !integral_dirac//= !indicE !in_setT/= !mul1e !diracE.
-rewrite !muleDr// -!addeA.
-by congr (_ + _)%E; rewrite ?addeA !muleA -?muleDl//;
-congr (_ * _)%E; congr (_%:E); field.
-Qed.
-
 End sample_pair.
 
 Section bernoulli_examples.
@@ -357,24 +336,23 @@ rewrite !integral_measure_add //=; last by move=> b _; rewrite integral_ge0.
 rewrite !ge0_integral_mscale //=; last 2 first.
   by move=> b _; rewrite integral_ge0.
   by move=> b _; rewrite integral_ge0.
-rewrite !integral_dirac// !indicE !in_setT !mul1e.
+rewrite !integral_dirac// !diracT !mul1e.
 rewrite iteE/= !ge0_integral_mscale//=.
 rewrite ger0_norm//.
 rewrite !integral_indic//= !iteE/= /mscale/=.
-rewrite setTI diracE !in_setT !mule1.
+rewrite setTI !diracT !mule1.
 rewrite ger0_norm//.
 rewrite -EFinD/= eqe ifF; last first.
   by apply/negbTE/negP => /orP[/eqP|//]; rewrite /onem; lra.
 rewrite !letin'E/= !iteE/=.
 rewrite !ge0_integral_mscale//=.
 rewrite ger0_norm//.
-rewrite !integral_dirac//= !indicE !in_setT /= !mul1e ger0_norm//.
+rewrite !integral_dirac//= !diracT !mul1e ger0_norm//.
 rewrite exp_var'E (execD_var_erefl "x")/=.
 rewrite /bernoulli/= measure_addE/= /mscale/= !mul1r.
-rewrite muleDl//; congr (_ + _)%E;
-  rewrite -!EFinM;
-  congr (_%:E);
-  by rewrite indicE /onem; case: (_ \in _); field.
+by rewrite muleDl//; congr (_ + _)%E;
+  rewrite -!EFinM; congr (_%:E);
+  rewrite !indicT !indicE /onem /=; case: (_ \in _); field.
 Qed.
 
 Definition bernoulli12_score := [Normalize
@@ -400,11 +378,11 @@ rewrite !integral_measure_add //=; last by move=> b _; rewrite integral_ge0.
 rewrite !ge0_integral_mscale //=; last 2 first.
   by move=> b _; rewrite integral_ge0.
   by move=> b _; rewrite integral_ge0.
-rewrite !integral_dirac// !indicE !in_setT !mul1e.
+rewrite !integral_dirac// !diracT !mul1e.
 rewrite iteE/= !ge0_integral_mscale//=.
 rewrite ger0_norm//.
 rewrite !integral_indic//= !iteE/= /mscale/=.
-rewrite setTI diracE !in_setT !mule1.
+rewrite setTI !diracT !mule1.
 rewrite ger0_norm//.
 rewrite -EFinD/= eqe ifF; last first.
   apply/negbTE/negP => /orP[/eqP|//].
@@ -412,13 +390,13 @@ rewrite -EFinD/= eqe ifF; last first.
 rewrite !letin'E/= !iteE/=.
 rewrite !ge0_integral_mscale//=.
 rewrite ger0_norm//.
-rewrite !integral_dirac//= !indicE !in_setT /= !mul1e ger0_norm//.
+rewrite !integral_dirac//= !diracT !mul1e ger0_norm//.
 rewrite exp_var'E (execD_var_erefl "x")/=.
 rewrite /bernoulli/= measure_addE/= /mscale/= !mul1r.
 rewrite muleDl//; congr (_ + _)%E;
   rewrite -!EFinM;
   congr (_%:E);
-  by rewrite indicE /onem; case: (_ \in _); field.
+  by rewrite !indicT !indicE /onem /=; case: (_ \in _); field.
 Qed.
 
 (* https://dl.acm.org/doi/pdf/10.1145/2933575.2935313 (Sect. 4) *)
@@ -447,13 +425,13 @@ under eq_integral.
   over.
 rewrite !integral_measure_add //=; last by move=> b _; rewrite integral_ge0.
 rewrite !ge0_integral_mscale //=; last 2 first.
-  by move=> b _; rewrite integral_ge0.
-  by move=> b _; rewrite integral_ge0.
-rewrite !integral_dirac// !indicE !in_setT !mul1e.
+  by move=> b _; exact: integral_ge0.
+  by move=> b _; exact: integral_ge0.
+rewrite !integral_dirac// !diracT !mul1e.
 rewrite iteE/= !ge0_integral_mscale//=.
 rewrite ger0_norm//.
-rewrite !integral_indic//= !iteE/= /mscale/=.
-rewrite setTI diracE !in_setT !mule1.
+rewrite !integral_cst//= !diracT !(mule1,mul1e).
+rewrite !iteE/= /mscale/= !diracT !mule1.
 rewrite ger0_norm//.
 rewrite -EFinD/= eqe ifF; last first.
   apply/negbTE/negP => /orP[/eqP|//].
@@ -461,12 +439,12 @@ rewrite -EFinD/= eqe ifF; last first.
 rewrite !letin'E/= !iteE/=.
 rewrite !ge0_integral_mscale//=.
 rewrite ger0_norm//.
-rewrite !integral_dirac//= !indicE !in_setT /= !mul1e ger0_norm//.
+rewrite !integral_dirac//= !diracT !mul1e ger0_norm//.
 rewrite /bernoulli/= measure_addE/= /mscale/= !mul1r.
 rewrite muleDl//; congr (_ + _)%E;
   rewrite -!EFinM;
   congr (_%:E);
-  by rewrite indicE /onem; case: (_ \in _); field.
+  by rewrite !indicT !indicE /onem /=; case: (_ \in _); field.
 Qed.
 
 End bernoulli_examples.
@@ -494,7 +472,7 @@ Proof.
 apply/eq_sfkernel => x U.
 rewrite letin'E/= /sample; unlock.
 rewrite integral_measure_add//= ge0_integral_mscale//= ge0_integral_mscale//=.
-rewrite integral_dirac//= integral_dirac//= !indicT/= !mul1e.
+rewrite !integral_dirac//= !diracT/= !mul1e.
 by rewrite /mscale/= iteE//= iteE//= fail'E mule0 adde0 ger0_norm.
 Qed.
 
diff --git a/theories/lang_syntax_toy.v b/theories/lang_syntax_toy.v
index a328ea1cd..2c2f57267 100644
--- a/theories/lang_syntax_toy.v
+++ b/theories/lang_syntax_toy.v
@@ -1,7 +1,7 @@
 Require Import String Classical.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg.
-From mathcomp.classical Require Import mathcomp_extra boolp.
+From mathcomp Require Import mathcomp_extra boolp.
 Require Import signed reals topology normedtype.
 Require Import lang_syntax_util.
 
@@ -36,7 +36,7 @@ Variables (R : realType).
 
 Inductive typ := Real | Unit.
 
-Canonical typ_eqType := Equality.Pack (@gen_eqMixin typ).
+HB.instance Definition _ := gen_eqMixin typ.
 
 Definition iter_pair (l : list Type) : Type :=
   foldr (fun x y => (x * y)%type) unit l.
@@ -169,7 +169,7 @@ Implicit Types str : string.
 
 Inductive typ := Real | Unit | Pair : typ -> typ -> typ.
 
-Canonical typ_eqType := Equality.Pack (@gen_eqMixin typ).
+HB.instance Definition _ := gen_eqMixin typ.
 
 Fixpoint mtyp (t : typ) : Type :=
   match t with
diff --git a/theories/lang_syntax_util.v b/theories/lang_syntax_util.v
index ad84918c9..608d25e7e 100644
--- a/theories/lang_syntax_util.v
+++ b/theories/lang_syntax_util.v
@@ -8,8 +8,7 @@ Require Import signed.
 (*                  Shared by lang_syntax_*.v files                           *)
 (******************************************************************************)
 
-Definition string_eqMixin := @EqMixin string String.eqb eqb_spec.
-Canonical string_eqType := EqType string string_eqMixin.
+HB.instance Definition _ := hasDecEq.Build string eqb_spec.
 
 Ltac inj_ex H := revert H;
   match goal with
diff --git a/theories/measure.v b/theories/measure.v
index 6ea3182fa..1733f4498 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -1181,32 +1181,24 @@ Lemma measurable_and (f : T1 -> bool) (g : T1 -> bool) :
   measurable_fun setT f -> measurable_fun setT g ->
   measurable_fun setT (fun x => f x && g x).
 Proof.
-move=> mf mg.
-apply: (@measurable_fun_bool _ _ true).
+move=> mf mg; apply: (@measurable_fun_bool _ _ true).
 rewrite [X in measurable X](_ : _ = f @^-1` [set true] `&` g @^-1` [set true]).
-apply: measurableI.
-rewrite -[X in measurable X]setTI.
-exact: mf.
-rewrite -[X in measurable X]setTI.
-exact: mg.
-apply/seteqP.
-by split; move=> x/andP.
+  apply: measurableI.
+  - rewrite -[X in measurable X]setTI; exact: mf.
+  - rewrite -[X in measurable X]setTI; exact: mg.
+by apply/seteqP; split => x /andP.
 Qed.
 
 Lemma measurable_or (f : T1 -> bool) (g : T1 -> bool) :
   measurable_fun setT f -> measurable_fun setT g ->
   measurable_fun setT (fun x => f x || g x).
 Proof.
-move=> mf mg.
-apply: (@measurable_fun_bool _ _ true).
+move=> mf mg; apply: (@measurable_fun_bool _ _ true).
 rewrite [X in measurable X](_ : _ = f @^-1` [set true] `|` g @^-1` [set true]).
-apply: measurableU.
-rewrite -[X in measurable X]setTI.
-exact: mf.
-rewrite -[X in measurable X]setTI.
-exact: mg.
-apply/seteqP.
-split; move=> x => /orP//.
+  apply: measurableU.
+  - rewrite -[X in measurable X]setTI; exact: mf.
+  - rewrite -[X in measurable X]setTI; exact: mg.
+by apply/seteqP; split=> x /orP.
 Qed.
 
 End measurable_fun.
diff --git a/theories/prob_lang.v b/theories/prob_lang.v
index d870d5072..54d075387 100644
--- a/theories/prob_lang.v
+++ b/theories/prob_lang.v
@@ -2,10 +2,10 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import rat.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
-From mathcomp.classical Require Import functions cardinality fsbigop.
+From mathcomp Require Import mathcomp_extra boolp classical_sets.
+From mathcomp Require Import functions cardinality fsbigop.
 Require Import reals ereal signed topology normedtype sequences esum measure.
-Require Import lebesgue_measure  numfun lebesgue_integral exp kernel.
+Require Import lebesgue_measure numfun lebesgue_integral exp kernel.
 
 (******************************************************************************)
 (*  Semantics of a probabilistic programming language using s-finite kernels  *)
@@ -86,7 +86,6 @@ Qed.
 
 Section bernoulli.
 Variables (R : realType) (p : {nonneg R}) (p1 : (p%:num <= 1)%R).
-Local Open Scope ring_scope.
 
 Definition bernoulli : set _ -> \bar R :=
   measure_add
@@ -95,8 +94,6 @@ Definition bernoulli : set _ -> \bar R :=
 
 HB.instance Definition _ := Measure.on bernoulli.
 
-Local Close Scope ring_scope.
-
 Let bernoulli_setT : bernoulli [set: _] = 1.
 Proof.
 rewrite /bernoulli/= /measure_add/= /msum 2!big_ord_recr/= big_ord0 add0e/=.
@@ -116,7 +113,7 @@ Lemma integral_bernoulli {R : realType}
 Proof.
 move=> f0.
 rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=.
-by rewrite !ge0_integral_mscale//= !integral_dirac//= indicT 2!mul1e.
+by rewrite !ge0_integral_mscale//= !integral_dirac//= !diracT !mul1e.
 Qed.
 
 Section uniform_probability.
@@ -131,7 +128,7 @@ HB.instance Definition _ := Measure.on uniform_probability.
 Let uniform_probability_setT : uniform_probability [set: _] = 1.
 Proof.
 rewrite /uniform_probability /mscale/= /mrestr/=.
-rewrite setTI lebesgue_measure_itv hlength_itv/= lte_fin.
+rewrite setTI lebesgue_measure_itv/= lte_fin.
 by rewrite -subr_gt0 ab0 -EFinD -EFinM mulVf// gt_eqF// subr_gt0.
 Qed.
 
@@ -528,7 +525,7 @@ Proof.
 apply/eq_measure/funext => U.
 rewrite /ite; unlock => /=.
 rewrite /kcomp/= integral_dirac//=.
-rewrite indicT mul1e.
+rewrite diracT mul1e.
 rewrite -/(measure_add (ITE.kiteT k1 (x, f x)) (ITE.kiteF k2 (x, f x))).
 rewrite measure_addE.
 rewrite /ITE.kiteT /ITE.kiteF/=.
@@ -588,7 +585,7 @@ Lemma letin_retk
   x U : measurable U ->
   letin (ret mf) k x U = k (x, f x) U.
 Proof.
-move=> mU; rewrite letinE retE integral_dirac ?indicT ?mul1e//.
+move=> mU; rewrite letinE retE integral_dirac ?diracT ?mul1e//.
 exact: (measurableT_comp (measurable_kernel k _ mU)).
 Qed.
 
@@ -893,7 +890,7 @@ Let kcomp_scoreE d1 d2 (T1 : measurableType d1) (T2 : measurableType d2)
   (score mf \; g) r U = `|f r|%:E * g (r, tt) U.
 Proof.
 rewrite /= /kcomp /kscore /= ge0_integral_mscale//=.
-by rewrite integral_dirac// indicT mul1e.
+by rewrite integral_dirac// diracT mul1e.
 Qed.
 
 Lemma scoreE d' (T' : measurableType d') (x : T * T') (U : set T') (f : R -> R)
@@ -926,7 +923,7 @@ Proof.
 apply/eq_sfkernel => x U.
 rewrite letinE/= /sample; unlock.
 rewrite integral_measure_add//= ge0_integral_mscale//= ge0_integral_mscale//=.
-rewrite integral_dirac//= integral_dirac//= !indicT/= !mul1e.
+rewrite integral_dirac//= integral_dirac//= !diracT/= !mul1e.
 by rewrite /mscale/= iteE//= iteE//= failE mule0 adde0 ger0_norm.
 Qed.
 
@@ -1004,24 +1001,23 @@ Let T0 z : (T z) set0 = 0. Proof. by []. Qed.
 Let T_ge0 z x : 0 <= (T z) x. Proof. by []. Qed.
 Let T_semi_sigma_additive z : semi_sigma_additive (T z).
 Proof. exact: measure_semi_sigma_additive. Qed.
-HB.instance Definition _ z := @isMeasure.Build _ R X (T z) (T0 z) (T_ge0 z)
+HB.instance Definition _ z := @isMeasure.Build _ X R (T z) (T0 z) (T_ge0 z)
   (@T_semi_sigma_additive z).
 
 Let sfinT z : sfinite_measure (T z). Proof. exact: sfinite_kernel_measure. Qed.
-HB.instance Definition _ z := @Measure_isSFinite_subdef.Build _ X R
-  (T z) (sfinT z).
+
+HB.instance Definition _ z := @isSFinite.Build _ X R (T z) (sfinT z).
 
 Definition U z : set Y -> \bar R := u z.
 Let U0 z : (U z) set0 = 0. Proof. by []. Qed.
 Let U_ge0 z x : 0 <= (U z) x. Proof. by []. Qed.
 Let U_semi_sigma_additive z : semi_sigma_additive (U z).
 Proof. exact: measure_semi_sigma_additive. Qed.
-HB.instance Definition _ z := @isMeasure.Build _ R Y (U z) (U0 z) (U_ge0 z)
+HB.instance Definition _ z := @isMeasure.Build _ Y R (U z) (U0 z) (U_ge0 z)
   (@U_semi_sigma_additive z).
 
 Let sfinU z : sfinite_measure (U z). Proof. exact: sfinite_kernel_measure. Qed.
-HB.instance Definition _ z := @Measure_isSFinite_subdef.Build _ Y R
-  (U z) (sfinU z).
+HB.instance Definition _ z := @isSFinite.Build _ Y R (U z) (sfinU z).
 
 Lemma letinC z A : measurable A ->
   letin t
@@ -1055,7 +1051,7 @@ End letinC.
 
 Section constants.
 Variable R : realType.
-Local Open Scope ring_scope.
+Local Close Scope ereal_scope.
 
 Lemma onem1S n : `1- (1 / n.+1%:R) = (n%:R / n.+1%:R)%:nng%:num :> R.
 Proof.
@@ -1063,7 +1059,7 @@ by rewrite /onem/= -{1}(@divrr _ n.+1%:R) ?unitfE// -mulrBl -natr1 addrK.
 Qed.
 
 Lemma p1S n : (1 / n.+1%:R)%:nng%:num <= 1 :> R.
-Proof. by rewrite ler_pdivr_mulr//= mul1r ler1n. Qed.
+Proof. by rewrite ler_pdivrMr//= mul1r ler1n. Qed.
 
 Lemma p12 : (1 / 2%:R)%:nng%:num <= 1 :> R. Proof. by rewrite p1S. Qed.
 
@@ -1073,7 +1069,7 @@ Lemma onem27 : `1- (2 / 7%:R) = (5%:R / 7%:R)%:nng%:num :> R.
 Proof. by apply/eqP; rewrite subr_eq/= -mulrDl -natrD divrr// unitfE. Qed.
 
 Lemma p27 : (2 / 7%:R)%:nng%:num <= 1 :> R.
-Proof. by rewrite /= lter_pdivr_mulr// mul1r ler_nat. Qed.
+Proof. by rewrite /= lter_pdivrMr// mul1r ler_nat. Qed.
 
 End constants.
 Arguments p12 {R}.
@@ -1145,7 +1141,7 @@ Lemma letin_sample_bernoulli d d' (T : measurableType d)
 Proof.
 rewrite letinE/=.
 rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=.
-by rewrite !ge0_integral_mscale//= !integral_dirac//= indicT 2!mul1e.
+by rewrite !ge0_integral_mscale//= !integral_dirac//= !diracT 2!mul1e.
 Qed.
 
 Section sample_and_return.
@@ -1327,8 +1323,8 @@ Qed.
 End staton_bus_exponential.
 
 (* X + Y is a measurableType if X and Y are *)
-Canonical sum_pointedType (X Y : pointedType) :=
-  PointedType (X + Y) (@inl X Y point).
+HB.instance Definition _ (X Y : pointedType) :=
+  isPointed.Build (X + Y)%type (@inl X Y point).
 
 Section measurable_sum.
 Context d d' (X : measurableType d) (Y : measurableType d').
@@ -1344,7 +1340,7 @@ Let sumU (F : (set (X + Y))^nat) : (forall i, measurable_sum (F i)) ->
 Proof. by []. Qed.
 
 HB.instance Definition _ := @isMeasurable.Build default_measure_display (X + Y)%type
-  (Pointed.class _) measurable_sum sum0 sumC sumU.
+  measurable_sum sum0 sumC sumU.
 
 End measurable_sum.
 
@@ -1485,7 +1481,7 @@ Proof. exact: sigma_algebra_bigcup. Qed.
 
 HB.instance Definition sum_salgebra_mixin :=
   @isMeasurable.Build (measure_sum_display (d1, d2))
-    (T1 + T2)%type (Pointed.class _) (image_classes f1 f2)
+    (T1 + T2)%type (image_classes f1 f2)
     (sum_salgebra_set0) (sum_salgebra_setC) (sum_salgebra_bigcup).
 
 End sum_salgebra_instance.
@@ -1748,9 +1744,9 @@ exists (fun n => [the R.-ker _ ~> _ of case_sum' (fun ab => [the R.-fker _ ~> _
   have [rfalse Hrfalse] := measure_uub (f (inr false) n).
   have [rtrue Hrtrue] := measure_uub (f (inr true) n).
   exists (maxr rtt (maxr rfalse rtrue)) => //= -[x [[]|[|]]] /=.
-  by rewrite 2!EFin_max lt_maxr Hrtt.
-  by rewrite /CASE_SUM.case_sumr /= 2!EFin_max 2!lt_maxr Hrtrue 2!orbT.
-  by rewrite /CASE_SUM.case_sumr /= 2!EFin_max 2!lt_maxr Hrfalse orbT.
+  by rewrite 2!EFin_max lt_max Hrtt.
+  by rewrite /CASE_SUM.case_sumr /= 2!EFin_max 2!lt_max Hrtrue 2!orbT.
+  by rewrite /CASE_SUM.case_sumr /= 2!EFin_max 2!lt_max Hrfalse orbT.
 move=> [x [[]|[|]]] U mU/=-.
 by rewrite (Hf (inl tt) x _ mU).
 by rewrite (Hf (inr true) x _ mU).
diff --git a/theories/prob_lang_wip.v b/theories/prob_lang_wip.v
index 9ab73014b..fd6716937 100644
--- a/theories/prob_lang_wip.v
+++ b/theories/prob_lang_wip.v
@@ -1,8 +1,8 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import rat.
-From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
-From mathcomp.classical Require Import functions cardinality fsbigop.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop.
 Require Import signed reals ereal topology normedtype sequences esum measure.
 Require Import lebesgue_measure  numfun lebesgue_integral exp kernel trigo.
 Require Import prob_lang.
@@ -81,7 +81,7 @@ rewrite /mgauss01/= integral_bigcup//=; last first.
   rewrite (_ : (fun x => _) = (EFin \o gauss01_density)); last first.
     by apply/funext => x; rewrite gee0_abs// lee_fin gauss_density_ge0.
   apply: le_lt_trans.
-    apply: (@subset_integral _ _ _ _ _ setT) => //=.
+    apply: (@ge0_subset_integral _ _ _ _ _ setT) => //=.
       apply/EFin_measurable_fun.
       exact: measurable_fun_gauss_density.
     by move=> ? _; rewrite lee_fin gauss_density_ge0.
@@ -142,7 +142,7 @@ transitivity (\int[@mgauss01 R]_(y in U) (f1 y)%:E).
   apply: eq_integral => //= r.
   rewrite letinE/= ge0_integral_mscale//= ger0_norm//; last first.
     by rewrite invr_ge0// gauss_density_ge0.
-  by rewrite integral_dirac// indicT mul1e diracE indicE.
+  by rewrite integral_dirac// diracT mul1e diracE indicE.
 rewrite integral_mgauss01//.
 transitivity (\int[lebesgue_measure]_(x in U) (\1_U x)%:E).
   apply: eq_integral => /= y yU.
@@ -196,7 +196,7 @@ rewrite /mpoisson1/= integral_bigcup//=; last first.
   rewrite (_ : (fun x => _) = (EFin \o poisson1)); last first.
     by apply/funext => x; rewrite gee0_abs// lee_fin poisson1_ge0//.
   apply: le_lt_trans.
-    apply: (@subset_integral _ _ _ _ _ setT) => //=.
+    apply: (@ge0_subset_integral _ _ _ _ _ setT) => //=.
       by apply/EFin_measurable_fun; exact: measurable_poisson.
     by move=> ? _; rewrite lee_fin poisson1_ge0//.
   by rewrite /= integral_poisson_density// ltry.