diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 3c897c12..548e6154 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -13,6 +13,7 @@ jobs:
         coq_container:
 #        - coqorg/coq:8.12.2
         - coqorg/coq:8.16.1-ocaml-4.13.1-flambda
+        - coqorg/coq:8.18.0-ocaml-4.13.1-flambda
     container:
       image: ${{ matrix.coq_container }}
       options: --user root
diff --git a/_CoqProject b/_CoqProject
index 2b7a0722..101bc735 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1 +1 @@
--R coq FormalML -arg -set -arg "Warnings=+default,-ambiguous-path,-typechecker,-ssr-search-moved,-deprecated,-notation-overridden"
\ No newline at end of file
+-R coq FormalML -arg -set -arg "Warnings=+default,-ambiguous-path,-coercions,-hiding-delimiting-key,-overwriting-delimiting-key,-redundant-canonical-projection,-typechecker,-ssr-search-moved,-deprecated,-notation-overridden"
\ No newline at end of file
diff --git a/coq/CertRL/LM/lax_milgram.v b/coq/CertRL/LM/lax_milgram.v
index 0c882aa5..1d860f94 100644
--- a/coq/CertRL/LM/lax_milgram.v
+++ b/coq/CertRL/LM/lax_milgram.v
@@ -1005,12 +1005,11 @@ intro x; field.
 repeat (rewrite Hx1 in HU0).
 rewrite Rmult_comm.
 trivial.
-absurd (norm u0 = 0).
+try revert HU0.
 apply Rgt_not_eq.
 apply Rlt_gt.
 apply norm_gt_0.
 trivial.
-trivial.
 apply norm_ge_0.
 simpl.
 apply is_finite_correct in Hfin.
diff --git a/coq/CertRL/qvalues.v b/coq/CertRL/qvalues.v
index 2cd1d048..e567ef20 100644
--- a/coq/CertRL/qvalues.v
+++ b/coq/CertRL/qvalues.v
@@ -444,10 +444,11 @@ Qed.
   Proof.
     destruct (is_nil_dec l); try now subst.
     apply Rle_antisym.
-    + rewrite Rmax_list_le_iff; try rewrite map_not_nil; try easy.
-      intros x Hx. rewrite in_map_iff in Hx.
-      destruct Hx as [x0 [Hx0 Hx0']].
-      now subst. congruence.
+    + rewrite Rmax_list_le_iff; try rewrite map_not_nil.
+      * intros x Hx. rewrite in_map_iff in Hx.
+        destruct Hx as [x0 [Hx0 Hx0']].
+        now subst.
+      * congruence.
     + apply Rmax_spec.
       rewrite in_map_iff.
       rewrite BasicUtils.ne_symm in n.
diff --git a/coq/FHE/encode.v b/coq/FHE/encode.v
index 4c8a6401..1e4e2f9c 100644
--- a/coq/FHE/encode.v
+++ b/coq/FHE/encode.v
@@ -1283,7 +1283,7 @@ Canonical ev_C_rmorphism (x:R[i]) := RMorphism (ev_C_is_rmorphism x).
   Proof.
     move=> p.
     rewrite /peval_C_quot -eq_lock.
-    case piP => a /EquivQuot.eqmodP.
+    case: piP => a /EquivQuot.eqmodP.
     rewrite /Quotient.equiv_equiv /Quotient.equiv /in_mem /mem /= /peval_C_ker_pred.
     destruct (ev_C_is_rmorphism x).
     rewrite base => eqq.
@@ -1713,7 +1713,7 @@ Section eval_vectors.
   Proof.
     move=> x.
     rewrite /mx_eval_quot -eq_lock.
-    case piP => a /EquivQuot.eqmodP.
+    case: piP => a /EquivQuot.eqmodP.
     rewrite /Quotient.equiv_equiv /Quotient.equiv /in_mem /mem /= /mx_eval_ker_pred.
     destruct mx_eval_is_rmorphism.
     rewrite base => eqq.
diff --git a/coq/NeuralNetworks/DefinedFunctions.v b/coq/NeuralNetworks/DefinedFunctions.v
index effaffa1..408fbb8e 100644
--- a/coq/NeuralNetworks/DefinedFunctions.v
+++ b/coq/NeuralNetworks/DefinedFunctions.v
@@ -11783,8 +11783,8 @@ Tactic Notation "DefinedFunction_scalar_cases" tactic(first) ident(c) :=
       intros fa.
       do 2 (apply functional_extensionality; intro).
       unfold scaleUnitVector; simpl.
-      match_destr.
-      now specialize (fa x1); simpl in fa.
+      match_destr
+      ; try now specialize (fa x1); simpl in fa.
     Qed.
 
 
diff --git a/coq/ProbTheory/ConditionalExpectation.v b/coq/ProbTheory/ConditionalExpectation.v
index 9c771479..ff2e155e 100644
--- a/coq/ProbTheory/ConditionalExpectation.v
+++ b/coq/ProbTheory/ConditionalExpectation.v
@@ -4293,7 +4293,7 @@ Section cond_exp_l2.
     unfold norm, minus, plus, opp in *; simpl in *.
     rewrite L2RRVq_norm_norm in HH2.
     autorewrite with quot in HH2.
-    rewrite LpRRVq_normE in HH2.
+    try rewrite LpRRVq_normE in HH2.
     rewrite LpRRVminus_plus.
     unfold nonneg in HH2 |- *; simpl in *.
     rewrite HH2.
@@ -4315,7 +4315,7 @@ Section cond_exp_l2.
         exists w'.
         split; trivial.
         autorewrite with quot.
-        rewrite LpRRVq_normE.
+        try rewrite LpRRVq_normE.
         now rewrite LpRRVminus_plus.
       + subst.
         exists (Quot _ w).
@@ -4324,7 +4324,7 @@ Section cond_exp_l2.
           split; trivial.
         * rewrite L2RRVq_norm_norm.
           autorewrite with quot.
-          rewrite LpRRVq_normE.
+          try rewrite LpRRVq_normE.
           now rewrite LpRRVminus_plus.
     } 
     repeat split.
@@ -4360,7 +4360,7 @@ Section cond_exp_l2.
           eauto.
         * rewrite L2RRVq_norm_norm.
           autorewrite with quot.
-          rewrite LpRRVq_normE.
+          try rewrite LpRRVq_normE.
           rewrite <- LpRRVminus_plus.
           unfold nonneg in *; simpl in *.
           rewrite xeqq.
@@ -4490,7 +4490,7 @@ Section cond_exp_l2.
         rewrite L2RRVq_norm_norm.
         unfold minus, plus, opp; simpl.
         LpRRVq_simpl.
-        rewrite LpRRVq_normE.
+        try rewrite LpRRVq_normE.
         now rewrite LpRRVminus_plus.
     - intros [?[??]]; subst.
       destruct H0 as [?[??]]; subst.
@@ -4500,7 +4500,7 @@ Section cond_exp_l2.
       rewrite L2RRVq_norm_norm.
       unfold minus, plus, opp; simpl.
       LpRRVq_simpl.
-      rewrite LpRRVq_normE.
+      try rewrite LpRRVq_normE.
       now rewrite LpRRVminus_plus.
   Qed.
 
diff --git a/coq/ProbTheory/Expectation.v b/coq/ProbTheory/Expectation.v
index f89637e2..a49bca46 100644
--- a/coq/ProbTheory/Expectation.v
+++ b/coq/ProbTheory/Expectation.v
@@ -1173,7 +1173,7 @@ Section Expectation_sec.
       + split; intros.
         * field_simplify in H.
           -- now apply INR_eq.
-          -- revert H.
+          -- try revert H.
              now apply pow_nzero.
         * subst.
           field_simplify; trivial.
@@ -4730,8 +4730,7 @@ Section EventRestricted.
       + typeclasses eauto.
       + intro z.
         unfold lift_event_restricted_domain_fun.
-        match_destr.
-        apply H5.
+        match_destr; try apply H5.
       + subst.
         erewrite event_restricted_SimpleExpectation; eauto.
         apply SimpleExpectation_ext.
@@ -4927,7 +4926,7 @@ Section indep.
         ; lra.
       } 
 
-      generalize (simple_approx_rv
+      generalize (simple_approx_rv (dom:= borel_sa)
                     (rvchoice (fun x => if Req_EM_T (c x) 0 then false else true)
                                        (fun x => x)
                                        (fun _ => 0)) n).
diff --git a/coq/ProbTheory/Martingale.v b/coq/ProbTheory/Martingale.v
index d5ff4f7a..ada6417a 100644
--- a/coq/ProbTheory/Martingale.v
+++ b/coq/ProbTheory/Martingale.v
@@ -1385,7 +1385,7 @@ Section martingale.
   Global Instance martingale_transform_adapted (H X : nat -> Ts -> R) sas
          {adapt:IsAdapted borel_sa X sas}
          {filt:IsFiltration sas} :
-    is_predictable H sas ->
+    is_predictable (saD:=borel_sa) H sas ->
     IsAdapted borel_sa (martingale_transform H X) sas.
   Proof.
     intros is_pre [|n]; simpl.
@@ -1419,7 +1419,7 @@ Section martingale.
         {isfeS:forall n, IsFiniteExpectation prts (rvmult (H (S n)) (rvminus (X (S n)) (X n)))}
         {isfe : forall n : nat, IsFiniteExpectation prts (martingale_transform H X n)}
         {adapt:IsAdapted borel_sa (martingale_transform H X) sas}
-        (predict: is_predictable H sas)
+        (predict: is_predictable (saD:=borel_sa) H sas)
         {mart:IsMartingale eq X sas} :
     IsMartingale eq (martingale_transform H X) sas.
   Proof.
@@ -1560,7 +1560,7 @@ Section martingale.
         {isfeS:forall n, IsFiniteExpectation prts (rvmult (H (S n)) (rvminus (X (S n)) (X n)))}
         {isfe : forall n : nat, IsFiniteExpectation prts (martingale_transform H X n)}
         {adapt:IsAdapted borel_sa (martingale_transform H X) sas}
-        (predict: is_predictable H sas)
+        (predict: is_predictable (saD:=borel_sa) H sas)
         (Hpos: forall n, almostR2 prts Rle (const 0) (H n))
         {mart:IsMartingale Rle X sas} :
     IsMartingale Rle (martingale_transform H X) sas.
diff --git a/coq/ProbTheory/MartingaleConvergence.v b/coq/ProbTheory/MartingaleConvergence.v
index 50f77e89..2fdcd2d9 100644
--- a/coq/ProbTheory/MartingaleConvergence.v
+++ b/coq/ProbTheory/MartingaleConvergence.v
@@ -167,7 +167,7 @@ Section mct.
                                    end)))).
             
     Lemma upcrossing_bound_is_predictable a b :
-      is_predictable (upcrossing_bound a b) sas.
+      is_predictable (saD:=borel_sa) (upcrossing_bound a b) sas.
     Proof.
       intros m.
       unfold upcrossing_bound.
@@ -2390,7 +2390,7 @@ Section mct.
       apply Rbar_plus_le_compat
       ; [| now rewrite IsFiniteNonnegExpectation; try reflexivity].
 
-      assert (ispredminus1:is_predictable (fun k : nat => rvminus (const 1) (upcrossing_bound Y a b k)) sas).
+      assert (ispredminus1:is_predictable (saD:=borel_sa) (fun k : nat => rvminus (const 1) (upcrossing_bound Y a b k)) sas).
       {
         red.
         apply is_adapted_minus.
diff --git a/coq/ProbTheory/MartingaleStopped.v b/coq/ProbTheory/MartingaleStopped.v
index dd92e081..af8e7810 100644
--- a/coq/ProbTheory/MartingaleStopped.v
+++ b/coq/ProbTheory/MartingaleStopped.v
@@ -166,7 +166,8 @@ Section stopped_process.
       forall n, RandomVariable dom borel_sa (process_stopped_at Y T n).
     Proof.
       intros.
-      eapply RandomVariable_proper; try apply process_stopped_at_as_alt; try reflexivity.
+      cut (RandomVariable dom borel_sa (process_stopped_at_alt Y T n))
+      ; [apply RandomVariable_proper; try reflexivity; apply process_stopped_at_as_alt; try reflexivity |].
       destruct n; simpl; trivial.
       apply rvplus_rv.
       - apply rvsum_rv; intros.
@@ -186,14 +187,17 @@ Section stopped_process.
       IsAdapted borel_sa (process_stopped_at Y T) F.
     Proof.
       intros n.
-      eapply (RandomVariable_proper _ (F n)); try apply process_stopped_at_as_alt; try reflexivity.
+      cut (RandomVariable (F n) borel_sa (process_stopped_at_alt Y T n))
+      ; [apply RandomVariable_proper; try reflexivity; apply process_stopped_at_as_alt; try reflexivity |].
       destruct n; simpl; trivial.
       apply rvplus_rv.
       - apply rvsum_rv_loc; intros.
         apply rvmult_rv; trivial.
-        + eapply (RandomVariable_proper_le (F m) _); try reflexivity.
-          * apply is_filtration_le; trivial; lia.
-          * apply adapt.
+        + cut (RandomVariable (F m) borel_sa (Y m)).
+          { eapply (RandomVariable_proper_le (F m) _); try reflexivity.
+            apply is_filtration_le; trivial; lia.
+          } 
+          apply adapt.
         + apply EventIndicator_pre_rv.
           generalize (is_stop m).
           apply is_filtration_le; trivial; lia.
diff --git a/coq/ProbTheory/RandomVariableFinite.v b/coq/ProbTheory/RandomVariableFinite.v
index 42a7501e..64aaeeff 100644
--- a/coq/ProbTheory/RandomVariableFinite.v
+++ b/coq/ProbTheory/RandomVariableFinite.v
@@ -1310,7 +1310,7 @@ Lemma Fatou_FiniteExpectation
 
 End fe.
 
-Hint Rewrite FiniteExpectation_const FiniteExpectation_plus FiniteExpectation_scale FiniteExpectation_opp FiniteExpectation_minus: prob.
+Hint Rewrite @FiniteExpectation_const @FiniteExpectation_plus @FiniteExpectation_scale @FiniteExpectation_opp @FiniteExpectation_minus: prob.
 
 Section ExpNonNeg.
   Context {Ts:Type} 
diff --git a/coq/ProbTheory/RandomVariableL2.v b/coq/ProbTheory/RandomVariableL2.v
index 98a8e537..cbef5e8f 100644
--- a/coq/ProbTheory/RandomVariableL2.v
+++ b/coq/ProbTheory/RandomVariableL2.v
@@ -768,7 +768,7 @@ Section L2.
   Proof.
     unfold Hnorm; simpl.
     LpRRVq_simpl.
-    rewrite LpRRVq_normE.
+    try rewrite LpRRVq_normE.
     unfold LpRRVnorm.
     unfold L2RRVinner.
     rewrite power_sqrt.
@@ -789,7 +789,7 @@ Section L2.
     rewrite LpRRVq_ballE.
     unfold minus, plus, opp; simpl.
     autorewrite with quot.
-    rewrite LpRRVq_normE.
+    try rewrite LpRRVq_normE.
     unfold LpRRVball.
     now rewrite LpRRVminus_plus.
   Qed.
@@ -815,7 +815,7 @@ Section L2.
     rewrite LpRRVq_ballE.
     unfold minus, plus, opp; simpl.
     autorewrite with quot.
-    rewrite LpRRVq_normE.
+    try rewrite LpRRVq_normE.
     unfold LpRRVball.
     erewrite LpRRV_norm_proper; [reflexivity |].
     rewrite LpRRVminus_plus.
@@ -859,7 +859,8 @@ Section L2.
       destruct (Quot_inv x); subst; simpl in *.
       unfold minus, plus, opp; simpl.
       autorewrite with quot.
-      rewrite LpRRVq_ballE, LpRRVq_normE.
+      rewrite LpRRVq_ballE.
+      try rewrite LpRRVq_normE.
       unfold LpRRVball.
       erewrite LpRRV_norm_proper; [reflexivity |].
       rewrite LpRRVminus_plus.
diff --git a/coq/ProbTheory/RandomVariableLinf.v b/coq/ProbTheory/RandomVariableLinf.v
index 4e5b9e1b..8815c594 100644
--- a/coq/ProbTheory/RandomVariableLinf.v
+++ b/coq/ProbTheory/RandomVariableLinf.v
@@ -2348,7 +2348,7 @@ End Linf.
       apply LiRRV_norm_sproper.
       intros ?; simpl.
       rv_unfold; lra.
-    - revert HH.
+    - try revert HH.
       apply pow_nzero.
       lra.
   Qed.
diff --git a/coq/ProbTheory/RandomVariableLpNat.v b/coq/ProbTheory/RandomVariableLpNat.v
index 38d28e9c..ccf6d690 100644
--- a/coq/ProbTheory/RandomVariableLpNat.v
+++ b/coq/ProbTheory/RandomVariableLpNat.v
@@ -1630,12 +1630,6 @@ Section Lp.
   
 End Lp.
 
-Hint Rewrite LpRRVq_constE : quot.
-Hint Rewrite LpRRVq_zeroE : quot.
-Hint Rewrite LpRRVq_scaleE : quot.
-Hint Rewrite LpRRVq_oppE : quot.
-Hint Rewrite LpRRVq_plusE : quot.
-Hint Rewrite LpRRVq_minusE : quot.
 Hint Rewrite @LpRRVq_constE : quot.
 Hint Rewrite @LpRRVq_zeroE : quot.
 Hint Rewrite @LpRRVq_scaleE : quot.
@@ -1643,7 +1637,13 @@ Hint Rewrite @LpRRVq_oppE : quot.
 Hint Rewrite @LpRRVq_plusE : quot.
 Hint Rewrite @LpRRVq_minusE : quot.
 Hint Rewrite @LpRRVq_constE : quot.
-Hint Rewrite LpRRVq_normE : quot.
+Hint Rewrite @LpRRVq_zeroE : quot.
+Hint Rewrite @LpRRVq_scaleE : quot.
+Hint Rewrite @LpRRVq_oppE : quot.
+Hint Rewrite @LpRRVq_plusE : quot.
+Hint Rewrite @LpRRVq_minusE : quot.
+Hint Rewrite @LpRRVq_constE : quot.
+Hint Rewrite @LpRRVq_normE : quot.
 
 Global Arguments LpRRVq_AbelianGroup {Ts} {dom} prts p.
 Global Arguments LpRRVq_ModuleSpace {Ts} {dom} prts p.
diff --git a/coq/ProbTheory/RandomVariableLpR.v b/coq/ProbTheory/RandomVariableLpR.v
index 513c8973..78985879 100644
--- a/coq/ProbTheory/RandomVariableLpR.v
+++ b/coq/ProbTheory/RandomVariableLpR.v
@@ -2143,12 +2143,6 @@ Qed.
 
 End Lp.
 
-Hint Rewrite LpRRVq_constE : quot.
-Hint Rewrite LpRRVq_zeroE : quot.
-Hint Rewrite LpRRVq_scaleE : quot.
-Hint Rewrite LpRRVq_oppE : quot.
-Hint Rewrite LpRRVq_plusE : quot.
-Hint Rewrite LpRRVq_minusE : quot.
 Hint Rewrite @LpRRVq_constE : quot.
 Hint Rewrite @LpRRVq_zeroE : quot.
 Hint Rewrite @LpRRVq_scaleE : quot.
@@ -2156,7 +2150,13 @@ Hint Rewrite @LpRRVq_oppE : quot.
 Hint Rewrite @LpRRVq_plusE : quot.
 Hint Rewrite @LpRRVq_minusE : quot.
 Hint Rewrite @LpRRVq_constE : quot.
-Hint Rewrite LpRRVq_normE : quot.
+Hint Rewrite @LpRRVq_zeroE : quot.
+Hint Rewrite @LpRRVq_scaleE : quot.
+Hint Rewrite @LpRRVq_oppE : quot.
+Hint Rewrite @LpRRVq_plusE : quot.
+Hint Rewrite @LpRRVq_minusE : quot.
+Hint Rewrite @LpRRVq_constE : quot.
+Hint Rewrite @LpRRVq_normE : quot.
 
 Global Arguments LpRRVq_AbelianGroup {Ts} {dom} prts p.
 Global Arguments LpRRVq_ModuleSpace {Ts} {dom} prts p.
@@ -2441,7 +2441,7 @@ Section complete.
       apply LpRRV_norm_sproper.
       intros ?; simpl.
       rv_unfold; lra.
-    - revert HH.
+    - try revert HH.
       apply pow_nzero.
       lra.
   Qed.
diff --git a/coq/ProbTheory/RbarExpectation.v b/coq/ProbTheory/RbarExpectation.v
index 0ff446cb..45732b37 100644
--- a/coq/ProbTheory/RbarExpectation.v
+++ b/coq/ProbTheory/RbarExpectation.v
@@ -1845,8 +1845,8 @@ Section EventRestricted.
       + typeclasses eauto.
       + intro z.
         unfold lift_event_restricted_domain_fun.
-        match_destr.
-        apply H5.
+        match_destr
+        ; try apply H5.
       + subst.
         erewrite event_restricted_SimpleExpectation; eauto.
         apply SimpleExpectation_ext.
@@ -4709,7 +4709,7 @@ Section rv_expressible.
           (X : nat -> Ts -> R) (n : nat) 
           (Y : Ts -> R)
           {rv_X : forall n, RandomVariable dom borel_sa (X n)}
-          {rv_y : RandomVariable (filtration_history_sa X n) borel_sa Y} :
+          {rv_y : RandomVariable (filtration_history_sa (cod:=borel_sa) X n) borel_sa Y} :
       exists g : vector R (S n) -> R,
          RandomVariable (Rvector_borel_sa (S n)) borel_sa g /\
          rv_eq Y (g ∘ (make_vector_from_seq X (S n))).
@@ -4736,7 +4736,7 @@ Section rv_expressible.
           (X : nat -> Ts -> R) (n : nat) 
           (g : vector R (S n) -> R)
           {rv_g : RandomVariable (Rvector_borel_sa (S n)) borel_sa g} :
-      RandomVariable (filtration_history_sa X n) borel_sa (g ∘ (make_vector_from_seq X (S n) )).
+      RandomVariable (filtration_history_sa (cod:=borel_sa) X n) borel_sa (g ∘ (make_vector_from_seq X (S n) )).
     Proof.
       rewrite filtrate_history_vector_equiv.
       now apply pullback_compose_rv.
diff --git a/coq/QLearn/Tsitsiklis.v b/coq/QLearn/Tsitsiklis.v
index 5ee98305..4a0325c5 100644
--- a/coq/QLearn/Tsitsiklis.v
+++ b/coq/QLearn/Tsitsiklis.v
@@ -7436,7 +7436,7 @@ End FixedPoint_contract.
     }
     apply rv_vecrvnth; intros.
     unfold vecrvnth.
-    eapply RandomVariable_proper; [reflexivity | reflexivity | ..].
+    eapply (RandomVariable_proper _ _ (reflexivity _) _ _ (reflexivity _)).
     - intros ?.
       unfold our_iso_f; simpl.
       unfold finite_fun_to_vector.
@@ -7717,7 +7717,7 @@ End FixedPoint_contract.
          intros.
          typeclasses eauto.
        } 
-       eapply RandomVariable_proper; [reflexivity | reflexivity | ..].
+       eapply (RandomVariable_proper _ _ (reflexivity _) _ _ (reflexivity _)).
        {
          intros ?.
          rewrite (FiniteExpectation_simple _ _).
diff --git a/coq/QLearn/qlearn_redux.v b/coq/QLearn/qlearn_redux.v
index f3262d2d..75ff8fab 100644
--- a/coq/QLearn/qlearn_redux.v
+++ b/coq/QLearn/qlearn_redux.v
@@ -1509,7 +1509,7 @@ Section stuff.
     intros.
     f_equal.
     generalize (ivector_sa_product vecps); intros.
-    pose (ve := ivector_create n (fun j _ => if i == j then (preimage_singleton (fun t : T => g t) a) else  Ω)).
+    pose (ve := ivector_create n (fun j _ => if i == j then (preimage_singleton (σd :=borel_sa) (fun t : T => g t) a) else  Ω)).
     specialize (H ve).
     rewrite (ivector_fold_left_Rmult_allbut_ident i pf) in H.
     - rewrite ivector_nth_map, ivector_nth_zip in H.
@@ -3039,6 +3039,7 @@ Lemma list_inter_prob_bound (l : list (event dom * R)) :
           subst kstar.
           field_simplify; try lra.
       + subst khat.
+        try intros H0.
         rewrite INR_up_pos in H0; try lra.
         generalize (up_pos _ r); intros.        
         assert (0 < up kstar)%Z by lia.
diff --git a/coq/QLearn/slln.v b/coq/QLearn/slln.v
index 99c71e05..fffe51cd 100644
--- a/coq/QLearn/slln.v
+++ b/coq/QLearn/slln.v
@@ -3192,8 +3192,8 @@ Qed.
   Proof.
     intros.
     assert (forall n,
-               sa_equiv (filtration_history_sa X n)
-                        (filtration_history_sa (fun n0 => (rvscale (/ b n0) (X n0))) n)).
+               sa_equiv (filtration_history_sa (cod:=borel_sa) X n)
+                        (filtration_history_sa (cod:=borel_sa) (fun n0 => (rvscale (/ b n0) (X n0))) n)).
     {
       intros.
       apply filtrate_sa_proper.
@@ -4296,7 +4296,8 @@ Qed.
       revert H.
       now apply independent_rv_collection_proper.
     }
-    generalize (filtration_history_sa_sub X); intros fsub.
+    generalize (filtration_history_sa_sub X (cod:=borel_sa)); intros fsub.
+
     generalize (independent_sas_split1 _ fsub H0 n); intros.
     unfold is_sub_algebras in H1.
     unfold independent_sas in *.
@@ -4315,7 +4316,7 @@ Qed.
     intros.
     apply independent_rv_sas.
     generalize (filtration_history_pullback_independent X H); intros.
-    assert (RandomVariable (filtration_history_sa X n) borel_sa (rvsum X n)).
+    assert (RandomVariable (filtration_history_sa (cod:=borel_sa) X n) borel_sa (rvsum X n)).
     {
       apply rvsum_rv_loc.
       intros.
@@ -4544,14 +4545,14 @@ Qed.
         {rv : forall n, RandomVariable dom borel_sa (X n)} 
         {rvdec : RandomVariable dom borel_sa (EventIndicator dec)} :
     independent_rv_collection Prts (const borel_sa) X ->    
-    sa_sigma (filtration_history_sa X n) P ->
+    sa_sigma (filtration_history_sa (cod:=borel_sa) X n) P ->
     independent_rvs Prts borel_sa borel_sa (X (S n)) (EventIndicator dec).
   Proof.
     intros.
     apply independent_rvs_symm.
     apply independent_rv_sas.
     generalize (filtration_history_pullback_independent X H n); intros.
-    assert (RandomVariable (filtration_history_sa X n) borel_sa (EventIndicator dec)) by
+    assert (RandomVariable (filtration_history_sa (cod:=borel_sa) X n) borel_sa (EventIndicator dec)) by
         now apply EventIndicator_pre_rv.
     generalize (pullback_rv_sub _ _ _ H2); intros.
     revert H1.
diff --git a/coq/lib_utils/LibUtilsStringAdd.v b/coq/lib_utils/LibUtilsStringAdd.v
index c9e5de93..67d43375 100644
--- a/coq/lib_utils/LibUtilsStringAdd.v
+++ b/coq/lib_utils/LibUtilsStringAdd.v
@@ -258,6 +258,8 @@ Module StringOrder <: OrderedTypeFull with Definition t:=string.
 
 End StringOrder.
 
+Global Existing Instance StringOrder.lt_strorder.
+
 (** * String prefixes *)
 
 Section Prefix.
@@ -342,11 +344,8 @@ Section Prefix.
     append (substring s n l) (substring (s+n) m l) = substring s (n+m) l.
   Proof.
     revert n m s.
-    induction l; simpl; destruct s; destruct n; simpl; trivial.
-    - f_equal.
-      apply IHl.
-    - rewrite IHl; simpl; trivial.
-    - rewrite IHl. simpl; trivial.
+    induction l; simpl; destruct s; destruct n; simpl; trivial
+    ; now rewrite IHl.
   Qed.
 
   Lemma substring_all l :
@@ -359,14 +358,8 @@ Section Prefix.
     substring s n l = substring s (min n (String.length l - s)) l.
   Proof.
     revert s n.
-    induction l; destruct s; destruct n; simpl; trivial.
-    - rewrite IHl; simpl.
-      f_equal.
-      f_equal.
-      f_equal.
-      lia.
-    - rewrite IHl.
-      match_case.
+    induction l; destruct s; destruct n; simpl; trivial
+    ; rewrite IHl; try rewrite Nat.sub_0_r; trivial.
   Qed.
 
   Lemma substring_le_prefix s n m l :
@@ -558,11 +551,11 @@ Section AsciiToString.
     StringOrder.lt s1 s2 -> ~StringOrder.eq s1 s2.
   Proof.
     compare s1 s2.
-    intros. rewrite e in *; clear e.
-    unfold not; intros.
-    apply asymmetry with (x := s2) (y := s2); assumption.
-    intros. assumption.
-    apply ascii_dec.
+    - intros. rewrite e in *; clear e.
+      intros ?.
+      apply asymmetry with (x := s2) (y := s2); assumption.
+    - intros. assumption.
+    - apply ascii_dec.
   Qed.
 
   Lemma lt_contr3 s :
diff --git a/coq/utils/DVector.v b/coq/utils/DVector.v
index ac99e4ee..8af2086e 100644
--- a/coq/utils/DVector.v
+++ b/coq/utils/DVector.v
@@ -311,8 +311,8 @@ Lemma vector_list_create_const_Forall {A} (c:A) start len :
 Proof.
   revert start.
   induction len; simpl; trivial; intros.
-  constructor; trivial.
-  now specialize (IHlen (S start)).
+  specialize (IHlen (S start)).
+  now constructor.
 Qed.
 
 Program Lemma vector_const_Forall {A} (c:A) n : Forall (fun a => a = c) (vector_const c n).
diff --git a/coq/utils/PairEncoding.v b/coq/utils/PairEncoding.v
index 4a3da1a3..f6fcf493 100644
--- a/coq/utils/PairEncoding.v
+++ b/coq/utils/PairEncoding.v
@@ -357,8 +357,7 @@ Lemma interleave_length_eq {A:Type} (l1 l2 : list A) :
   length (interleave l1 l2) = length l1 + length l2.
 Proof.
   revert l2.
-  induction l1; destruct l2; simpl in *; trivial.
-  - auto.
+  induction l1; destruct l2; simpl in *; auto.
   - rewrite IHl1.
     lia.
 Qed.
diff --git a/coq/utils/Quotient.v b/coq/utils/Quotient.v
index 688eb9cf..926f181d 100644
--- a/coq/utils/Quotient.v
+++ b/coq/utils/Quotient.v
@@ -16,7 +16,7 @@ Section quotient.
        | (y::l)::ll' =>
          match x == y with
          | left _ => (x::y::l)::ll'
-         | right_ => (y::l)::(add_to_bucket x ll')
+         | _right_ => (y::l)::(add_to_bucket x ll')
          end
        end.
 
diff --git a/coq/utils/nvector.v b/coq/utils/nvector.v
index 890fe82c..8e14a0d7 100644
--- a/coq/utils/nvector.v
+++ b/coq/utils/nvector.v
@@ -165,7 +165,7 @@ End Tensor.
 
 Inductive NumericType
   := FloatType
-   | IntTYpe.
+   | IntType.
 
 
 Definition ntype_interp (n:NumericType) : Type