diff --git a/theories/abel.v b/theories/abel.v
index 17e5f2d..0271684 100644
--- a/theories/abel.v
+++ b/theories/abel.v
@@ -1,3 +1,4 @@
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field polyrcf.
 From Abel Require Import various classic_ext map_gal algR.
@@ -456,7 +457,7 @@ apply/eqP; rewrite /image_mem (map_comp (fun i => x * w ^+ i)) val_enum_ord.
 rewrite -[p]prednK//= mulr1 -[p.-1]prednK//= expr1 !adjoin_cons.
 have -> : <<<<E; x>>; x * w>>%VS = <<<<E; w>>; x>>%VS.
   apply/eqP; rewrite [X in _ == X]adjoinC eqEsubv/= !Fadjoin_sub//.
-    by rewrite -(@fpredMl _ _ _ _ x)// ?memv_adjoin//= adjoinC memv_adjoin.
+    by rewrite -(@fpredMl _ _ x)// ?memv_adjoin//= adjoinC memv_adjoin.
   by rewrite rpredM// ?memv_adjoin//= adjoinC memv_adjoin.
 rewrite (Fadjoin_seq_idP _)// all_map; apply/allP => i _/=.
 by rewrite rpredM ?rpredX//= ?memv_adjoin// adjoinC memv_adjoin.
@@ -657,7 +658,8 @@ apply: classic_bind (@classic_fieldExtFor _ _ (p : {poly F^o}) p_neq0).
     exists rs => //; suff <- : limg iota = 1%VS by [].
     apply/eqP; rewrite eqEsubv sub1v andbT; apply/subvP => v.
     by move=> /memv_imgP[u _ ->]; rewrite iotaF/= rpredZ// rpred1.
-  pose S := SplittingFieldType F L splitL.
+    pose sM := FieldExt_isSplittingField.Build F L splitL.
+    pose S : splittingFieldType F := HB.pack L sM.
   exists S, rs; split => //=; first by rewrite -(eq_map_poly iotaF).
   by apply: (sol_p S rs); rewrite -(eq_map_poly iotaF).
 move=> L rs prs; apply: sol_p => -[M [rs' [prs']]].
@@ -682,7 +684,8 @@ have splitK : splittingFieldFor 1 (p ^^ in_alg K) fullv.
   by rewrite lfunE subvsP.
 have sfK : SplittingField.axiom K.
   by exists (p ^^ in_alg K) => //; apply/polyOver1P; exists p.
-pose S := SplittingFieldType F K sfK.
+pose sM := FieldExt_isSplittingField.Build F K sfK.
+pose S : splittingFieldType F := HB.pack K sM.
 have splitS : splittingFieldFor 1 (p ^^ in_alg S) fullv by [].
 have splitM : splittingFieldFor 1 (p ^^ in_alg M) <<1 & rs'>> by exists rs'.
 have splitL : splittingFieldFor 1 (p ^^ in_alg L) <<1 & rs>> by exists rs.
@@ -719,7 +722,8 @@ have splitL : SplittingField.axiom L.
   exists rs => //; suff <- : limg f = 1%VS by [].
   apply/eqP; rewrite eqEsubv sub1v andbT; apply/subvP => v.
   by move=> /memv_imgP[u _ ->]; rewrite fF/= rpredZ// rpred1.
-pose S := SplittingFieldType F L splitL.
+pose sM := FieldExt_isSplittingField.Build F L splitL.
+pose S : splittingFieldType F := HB.pack L sM.
 pose d := \dim  <<1 & (rs : seq S)>>.
 have /classic_cycloSplitting-/(_ S) : d%:R != 0 :> F.
   by have /charf0P-> := charF0; rewrite -lt0n adim_gt0.
@@ -750,7 +754,9 @@ have prs : p ^^ in_alg L %= \prod_(z <- rs) ('X - z%:P).
   by rewrite (eq_map_poly (fmorph_eq_rat _)).
 have splitL : SplittingField.axiom L.
   by exists (p ^^ in_alg L); [by apply/polyOver1P; exists p | exists rs].
-pose S := SplittingFieldType rat L splitL.
+pose Frat := [the fieldType of rat : Type].
+pose sM := FieldExt_isSplittingField.Build Frat L splitL.
+pose S : splittingFieldType Frat := HB.pack L sM.
 pose d := \dim <<1 & (rs : seq S)>>.
 have d_gt0 : (d > 0)%N by rewrite adim_gt0.
 have [ralg ralg_prim] := C_prim_root_exists d_gt0.
@@ -767,7 +773,8 @@ have splitL' : SplittingField.axiom L'.
   have [us cycloE usw] := splitting_Fadjoin_cyclotomic 1%AS w_prim.
   exists (us ++ rs'); last by rewrite adjoin_cat usw -adjoin_cons.
   by rewrite big_cat/= (eqp_trans (eqp_mulr _ cycloE))// eqp_mull//.
-pose S' := SplittingFieldType rat L' splitL'.
+pose sM' := FieldExt_isSplittingField.Build Frat L' splitL'.
+pose S' : splittingFieldType Frat := HB.pack L' sM'.
 have splitS : splittingFieldFor 1 (p ^^ in_alg S) fullv by exists rs.
 have splitS' : splittingFieldFor 1 (p ^^ in_alg S') <<1 & rs'>> by exists rs'.
 have [f /= imgf] := splitting_ahom splitS splitS'.
@@ -778,10 +785,10 @@ Qed.
 Lemma splitting_num_field (p : {poly rat}) :
   {L : splittingFieldType rat & { LtoC : {rmorphism L -> algC} |
     (p != 0 -> splittingFieldFor 1 (p ^^ in_alg L) {:L})
-    /\ (p = 0 -> L = [splittingFieldType rat of rat^o]) }}.
+    /\ (p = 0 -> L = [the splittingFieldType rat of rat^o]) }}.
 Proof.
 have [->|p_neq0] := eqVneq p 0.
-  by exists [splittingFieldType rat of rat^o], [rmorphism of ratr]; split.
+  by exists [the splittingFieldType rat of rat^o], [rmorphism of ratr]; split.
 have [/= rsalg pE] := closed_field_poly_normal (p ^^ (ratr : _ -> algC)).
 have {}pE : p ^^ ratr %= \prod_(z <- rsalg) ('X - z%:P).
   by rewrite pE (eqp_trans (eqp_scale _ _)) ?eqpxx// lead_coef_eq0 map_poly_eq0.
@@ -791,7 +798,10 @@ have splitL' : splittingFieldFor 1 (p ^^ in_alg L') {: L'}%AS.
   by rewrite -map_poly_comp map_prod_XsubC rs'E (eq_map_poly (fmorph_eq_rat _)).
 have splitaxL' : SplittingField.axiom L'.
   by exists (p ^^ in_alg L'); first by apply/polyOver1P; exists p.
-exists (SplittingFieldType rat L' splitaxL'), L'toC; split => //.
+pose Frat := [the fieldType of rat : Type].
+pose sM' := FieldExt_isSplittingField.Build Frat L' splitaxL'.
+pose S' : splittingFieldType Frat := HB.pack L' sM'.
+exists S', L'toC; split => //.
 by move=> p_eq0; rewrite p_eq0 eqxx in p_neq0.
 Qed.
 
@@ -811,7 +821,7 @@ Qed.
 Definition numfield (p : {poly rat}) : splittingFieldType rat :=
   projT1 (splitting_num_field p).
 
-Lemma numfield0 : numfield 0 = [splittingFieldType rat of rat^o].
+Lemma numfield0 : numfield 0 = [the splittingFieldType rat of rat^o].
 Proof. by rewrite /numfield; case: splitting_num_field => //= ? [? [_ ->]]. Qed.
 
 Definition numfield_inC (p : {poly rat}) :
@@ -901,7 +911,7 @@ Qed.
 Let rp'_uniq : uniq rp'.
 Proof.
 rewrite -separable_prod_XsubC -(eqp_separable ratr_p').
-rewrite -char0_ratrE separable_map.
+rewrite -char0_ratrE separable_map separable_poly.unlock.
 apply/coprimepP => d; have [sp_gt1 eqp] := p_irr => /eqp.
 rewrite size_poly_eq1; have [//|dN1 /(_ isT)] := boolP (d %= 1).
 move=> /eqp_dvdl-> /dvdp_leq; rewrite -size_poly_eq0 polyorder.size_deriv.
@@ -1073,7 +1083,7 @@ Lemma gal_perm_cycle_order : #[(gal_perm gal_cycle)]%g = d.
 Proof. by rewrite order_injm ?gal_cycle_order ?injm_gal_perm ?gal1. Qed.
 
 Definition conjL : {lrmorphism L -> L} :=
-  projT1 (restrict_aut_to_normal_num_field iota conjC).
+  projT1 (restrict_aut_to_normal_num_field iota Num.conj_op).
 
 Definition iotaJ : {morph iota : x / conjL x >-> x^*} :=
   projT2 (restrict_aut_to_normal_num_field _ _).
@@ -1209,6 +1219,7 @@ Hint Resolve irreducible_example : core.
 
 Lemma separable_example : separable_poly poly_example.
 Proof.
+rewrite separable_poly.unlock.
 apply/coprimepP => q /(irredp_XsubCP irreducible_example) [//| eqq].
 have size_deriv_example : size poly_example^`() = 5%N.
   rewrite !derivCE addr0 alg_polyC -scaler_nat addr0.
@@ -1269,7 +1280,7 @@ apply: lt_sorted_eq; rewrite ?sorted_roots//.
  by rewrite /= andbT -subr_gt0 opprK ?addr_gt0 ?alpha_gt0.
 move=> x; rewrite mem_rootsR ?map_poly_eq0// !inE -topredE/= orbC.
 rewrite deriv_poly_example /root.
-rewrite rmorphB linearZ/= map_polyC/= map_polyXn !pesimp.
+rewrite rmorphB /= linearZ map_polyC/= map_polyXn !pesimp.
 rewrite -[5%:R]sqr_sqrtr ?ler0n// (exprM _ 2 2) -exprMn (natrX _ 2 2) subr_sqr.
 rewrite mulf_eq0 [_ + 2%:R == 0]gt_eqF ?orbF; last first.
   by rewrite ltr_spaddr ?ltr0n// mulr_ge0 ?sqrtr_ge0// exprn_even_ge0.
@@ -1295,7 +1306,7 @@ rewrite -big_filter (perm_big (map algRval (rootsR pR))); last first.
   rewrite map_poly_comp/=.
   apply/andP/mapP => [[xR xroot]|[y + ->]].
     exists (in_algR xR); rewrite // mem_rootsR// -topredE/=.
-    by rewrite -(mapf_root algRval_rmorphism)/=.
+    by rewrite -(mapf_root [rmorphism of algRval])/=.
   rewrite mem_rootsR// -[y \in _]topredE/=.
   by split; [apply/algRvalP|rewrite mapf_root].
 apply/eqP; rewrite sum1_size size_map eqn_leq.
@@ -1354,12 +1365,7 @@ Definition decode_const (n : nat) : const :=
    match n with 0 => Zero | 1 => One | n.+2 => URoot n end.
 Lemma code_constK : cancel encode_const decode_const.
 Proof. by case. Qed.
-Definition const_eqMixin := CanEqMixin code_constK.
-Canonical const_eqType := EqType const const_eqMixin.
-Definition const_choiceMixin := CanChoiceMixin code_constK.
-Canonical const_choiceType := ChoiceType const const_choiceMixin.
-Definition const_countMixin := CanCountMixin code_constK.
-Canonical const_countType := CountType const const_countMixin.
+HB.instance Definition _ := Countable.copy const (can_type code_constK).
 
 Definition encode_binOp (c : binOp) : bool :=
    match c with Add => false | Mul => true end.
@@ -1367,12 +1373,7 @@ Definition decode_binOp (b : bool) : binOp :=
    match b with false => Add | _ => Mul end.
 Lemma code_binOpK : cancel encode_binOp decode_binOp.
 Proof. by case. Qed.
-Definition binOp_eqMixin := CanEqMixin code_binOpK.
-Canonical binOp_eqType := EqType binOp binOp_eqMixin.
-Definition binOp_choiceMixin := CanChoiceMixin code_binOpK.
-Canonical binOp_choiceType := ChoiceType binOp binOp_choiceMixin.
-Definition binOp_countMixin := CanCountMixin code_binOpK.
-Canonical binOp_countType := CountType binOp binOp_countMixin.
+HB.instance Definition _ := Countable.copy binOp (can_type code_binOpK).
 
 Definition encode_unOp (c : unOp) : nat + nat :=
    match c with Opp => inl _ 0%N | Inv => inl _ 1%N
@@ -1382,12 +1383,7 @@ Definition decode_unOp (n : nat + nat) : unOp :=
            | inl n.+2 => Exp n | inr n => Root n end.
 Lemma code_unOpK : cancel encode_unOp decode_unOp.
 Proof. by case. Qed.
-Definition unOp_eqMixin := CanEqMixin code_unOpK.
-Canonical unOp_eqType := EqType unOp unOp_eqMixin.
-Definition unOp_choiceMixin := CanChoiceMixin code_unOpK.
-Canonical unOp_choiceType := ChoiceType unOp unOp_choiceMixin.
-Definition unOp_countMixin := CanCountMixin code_unOpK.
-Canonical unOp_countType := CountType unOp unOp_countMixin.
+HB.instance Definition _ := Countable.copy unOp (can_type code_unOpK).
 
 Fixpoint encode_algT F (f : algterm F) : GenTree.tree (F + const) :=
   let T_ isbin := if isbin then binOp else unOp in
@@ -1414,14 +1410,12 @@ Lemma code_algTK F : cancel (@encode_algT F) (@decode_algT F).
 Proof.
 by elim => // [u f IHf|b f IHf f' IHf']/=; rewrite pickleK -lock ?IHf ?IHf'.
 Qed.
-Definition algT_eqMixin (F : eqType) := CanEqMixin (@code_algTK F).
-Canonical algT_eqType (F : eqType) := EqType (algterm F) (@algT_eqMixin F).
-Definition algT_choiceMixin (F : choiceType) := CanChoiceMixin (@code_algTK F).
-Canonical algT_choiceType (F : choiceType) :=
-  ChoiceType (algterm F) (@algT_choiceMixin F).
-Definition algT_countMixin (F : countType) := CanCountMixin (@code_algTK F).
-Canonical algT_countType (F : countType) :=
-  CountType (algterm F) (@algT_countMixin F).
+HB.instance Definition _ (F : eqType) := Equality.copy (algterm F)
+  (can_type (@code_algTK F)).
+HB.instance Definition _ (F : choiceType) := Choice.copy (algterm F)
+  (can_type (@code_algTK F)).
+HB.instance Definition _ (F : countType) := Countable.copy (algterm F)
+  (can_type (@code_algTK F)).
 
 Declare Scope algT_scope.
 Delimit Scope algT_scope with algT.
@@ -1551,7 +1545,9 @@ have mprs : mp ^^ in_alg L %= \prod_(z <- rsmp) ('X - z%:P).
   by rewrite -char0_ratrE// (eq_map_poly (fmorph_eq_rat _)) eqpxx.
 have splitL : SplittingField.axiom L.
   by exists (mp ^^ in_alg L); [apply/polyOver1P; exists mp | exists rsmp].
-pose S := SplittingFieldType rat L splitL.
+pose Frat := [the fieldType of rat : Type].
+pose sM := FieldExt_isSplittingField.Build Frat L splitL.
+pose S : splittingFieldType Frat := HB.pack L sM.
 have algsW: {subset rsalg <= algs}.
   move=> x; rewrite -fsE => /mapP[{x}f ffs ->].
   apply/flattenP; exists (subeval ratr f); rewrite ?map_f//.
@@ -1573,7 +1569,7 @@ rewrite {p p_neq0 mkalg pE prs rsmp iota_rs mprs rsf rs rsE mp
 suff: forall (L : splittingFieldType rat) (iota : {rmorphism L -> algC}) als,
         map iota als = algs -> radical.-ext 1%VS <<1 & als>>%VS.
   by move=> /(_ S iota als alsE).
-move=> {}L {}iota {splitL S} {}als {}alsE; rewrite {}/algs in alsE.
+move=> {sM}L {}iota {splitL S} {}als {}alsE; rewrite {}/algs in alsE.
 elim: fs => [|f fs IHfs]//= in rsalg fsE als alsE *.
   case: als => []// in alsE *.
   by rewrite Fadjoin_nil; apply: rext_refl.
diff --git a/theories/xmathcomp/algR.v b/theories/xmathcomp/algR.v
index d16fcc2..033a402 100644
--- a/theories/xmathcomp/algR.v
+++ b/theories/xmathcomp/algR.v
@@ -1,3 +1,4 @@
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field.
 From Abel Require Import various.
@@ -15,37 +16,23 @@ Local Notation "p ^^ f" := (map_poly f p)
 
 Record algR := in_algR {algRval : algC; algRvalP : algRval \is Num.real}.
 
-Canonical algR_subType := [subType for algRval].
-Definition algR_eqMixin := [eqMixin of algR by <:].
-Canonical algR_eqType := EqType algR algR_eqMixin.
-Definition algR_choiceMixin := [choiceMixin of algR by <:].
-Canonical algR_choiceType := ChoiceType algR algR_choiceMixin.
-Definition algR_countMixin := [countMixin of algR by <:].
-Canonical algR_countType := CountType algR algR_countMixin.
-Definition algR_zmodMixin := [zmodMixin of algR by <:].
-Canonical algR_zmodType := ZmodType algR algR_zmodMixin.
-Definition algR_ringMixin := [ringMixin of algR by <:].
-Canonical algR_ringType := RingType algR algR_ringMixin.
-Definition algR_comRingMixin := [comRingMixin of algR by <:].
-Canonical algR_comRingType := ComRingType algR algR_comRingMixin.
-Definition algR_unitRingMixin := [unitRingMixin of algR by <:].
-Canonical algR_unitRingType := UnitRingType algR algR_unitRingMixin.
-Canonical algR_comUnitRingType := [comUnitRingType of algR].
-Definition algR_idomainMixin := [idomainMixin of algR by <:].
-Canonical algR_idomainType := IdomainType algR algR_idomainMixin.
-Definition algR_fieldMixin := [fieldMixin of algR by <:].
-Canonical algR_fieldType := FieldType algR algR_fieldMixin.
-Definition algR_porderMixin := [porderMixin of algR by <:].
-Canonical algR_porderType := POrderType ring_display algR algR_porderMixin.
-Lemma total_algR : totalPOrderMixin [porderType of algR].
+HB.instance Definition _ := [isSub for algRval].
+HB.instance Definition _ := [Countable of algR by <:].
+HB.instance Definition _ := [SubChoice_isSubIntegralDomain of algR by <:].
+HB.instance Definition _ := [SubIntegralDomain_isSubField of algR by <:].
+HB.instance Definition _ := [POrder of algR by <:].
+Lemma total_algR : total (<=%O : rel [porderType of algR]).
 Proof. by move=> x y; apply/real_leVge/valP/valP. Qed.
-Canonical algR_latticeType := LatticeType algR total_algR.
-Canonical algR_distrLatticeType := DistrLatticeType algR total_algR.
-Canonical algR_orderType := OrderType algR total_algR.
+HB.instance Definition _ := Order.POrder_isTotal.Build _ algR total_algR.
 
-Lemma algRval_is_rmorphism : rmorphism algRval. Proof. by []. Qed.
-Canonical algRval_additive := Additive algRval_is_rmorphism.
-Canonical algRval_rmorphism := RMorphism algRval_is_rmorphism.
+Lemma algRval_is_additive : additive algRval. Proof. by []. Qed.
+Lemma algRval_is_multiplicative : multiplicative algRval. Proof. by []. Qed.
+HB.instance Definition _ :=
+  GRing.isAdditive.Build [zmodType of algR] [zmodType of algC] algRval
+    algRval_is_additive.
+HB.instance Definition _ :=
+  GRing.isMultiplicative.Build [ringType of algR] [ringType of algC] algRval
+    algRval_is_multiplicative.
 
 Definition algR_norm (x : algR) : algR := in_algR (normr_real (val x)).
 Lemma algR_ler_norm_add x y : algR_norm (x + y) <= (algR_norm x + algR_norm y).
@@ -58,8 +45,6 @@ Lemma algR_normrN x : algR_norm (- x) = algR_norm x.
 Proof. by apply/val_inj; apply: normrN. Qed.
 
 Section Num.
-Definition algR_normedMixin :=
-  Num.NormedMixin algR_ler_norm_add algR_normr0_eq0 algR_normrMn algR_normrN.
 
 Section withz.
 Let z : algR := 0.
@@ -73,18 +58,10 @@ Lemma algR_ler_def (x y : algR) : (x <= y) = (algR_norm (y - x) == y - x).
 Proof. by apply: ler_def. Qed.
 End withz.
 
-Let algR_ring := (GRing.Ring.Pack (GRing.ComRing.base
-  (GRing.ComUnitRing.base (GRing.IntegralDomain.base
-     (GRing.IntegralDomain.class [idomainType of algR]))))).
-Definition algR_numMixin : @Num.mixin_of algR_ring _ _ :=
-    @Num.Mixin _ _ algR_normedMixin
-      algR_addr_gt0 algR_ger_leVge algR_normrM algR_ler_def.
-
-Canonical algR_numDomainType  := NumDomainType algR algR_numMixin.
-Canonical algR_normedZmodType := NormedZmodType algR algR algR_normedMixin.
-Canonical algR_numFieldType := [numFieldType of algR].
-Canonical algR_realDomainType := [realDomainType of algR].
-Canonical algR_realFieldType := [realFieldType of algR].
+HB.instance Definition _ := Num.Zmodule_isNormed.Build _ algR
+  algR_ler_norm_add algR_normr0_eq0 algR_normrMn algR_normrN.
+HB.instance Definition _ := Num.isNumRing.Build algR
+  algR_addr_gt0 algR_ger_leVge algR_normrM algR_ler_def.
 End Num.
 
 Definition algR_archiFieldMixin : Num.archimedean_axiom [numDomainType of algR].
@@ -96,7 +73,8 @@ set n := floorC _; have [n_lt0|n_ge0] := ltP n 0.
 move=> x_lt; exists (`|(n + 1)%R|%N); apply: lt_le_trans x_lt _.
 by rewrite /= rmorphMn/= pmulrn gez0_abs// addr_ge0.
 Qed.
-Canonical algR_archiFieldType := ArchiFieldType algR algR_archiFieldMixin.
+HB.instance Definition _ := Num.RealField_isArchimedean.Build algR
+  algR_archiFieldMixin.
 
 Definition algRpfactor (x : algC) : {poly algR} :=
   if x \is Num.real =P true is ReflectT xR then 'X - (in_algR xR)%:P else
@@ -205,7 +183,7 @@ elim: n r => // n IHn [|x r]/= in p pr *.
 rewrite ltnS => r_lt.
 have xJxr : x^* \in x :: r.
   rewrite -root_prod_XsubC -pr.
-  have /eq_map_poly-> : algRval =1 conjC \o algRval.
+  have /eq_map_poly-> : algRval =1 Num.conj_op \o algRval.
     by move=> a /=; rewrite (CrealP (algRvalP _)).
   by rewrite map_poly_comp mapf_root pr root_prod_XsubC mem_head.
 have xJr : (x \isn't Num.real) ==> (x^* \in r) by rewrite implyNb CrealE.
@@ -270,4 +248,4 @@ move=> /andP[xR rsabR] /andP[axb arsb] prsab.
 exists (in_algR xR) => //=.
 by rewrite -(mapf_root [rmorphism of algRval])//= prsab rootM root_XsubC eqxx.
 Qed.
-Canonical algR_rcfType := RcfType algR algR_rcfMixin.
+HB.instance Definition _ := Num.RealField_isClosed.Build algR algR_rcfMixin.
diff --git a/theories/xmathcomp/char0.v b/theories/xmathcomp/char0.v
index 49ea16d..e81562a 100644
--- a/theories/xmathcomp/char0.v
+++ b/theories/xmathcomp/char0.v
@@ -1,3 +1,4 @@
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra all_field.
 
 Set Implicit Arguments.
@@ -45,16 +46,12 @@ Hypothesis charF0 : has_char0 F.
 
 Local Notation ratrF := (char0_ratr charF0).
 
-Fact char0_ratr_is_rmorphism : rmorphism ratrF.
+Fact char0_ratr_is_additive : additive ratrF.
 Proof.
 rewrite /char0_ratr.
 have injZtoQ: @injective rat int intr by apply: intr_inj.
 have nz_den x: (denq x)%:~R != 0 :> F by rewrite char0_intr_eq0 // denq_eq0.
-do 2?split; rewrite /ratr ?divr1 // => x y; last first.
-  rewrite mulrC mulrAC; apply: canLR (mulKf (nz_den _)) _; rewrite !mulrA.
-  do 2!apply: canRL (mulfK (nz_den _)) _; rewrite -!rmorphM; congr _%:~R.
-  apply: injZtoQ; rewrite !rmorphM [x * y]lock /= !numqE -lock.
-  by rewrite -!mulrA mulrA mulrCA -!mulrA (mulrCA y).
+rewrite /ratr ?divr1 // => x y.
 apply: (canLR (mulfK (nz_den _))); apply: (mulIf (nz_den x)).
 rewrite mulrAC mulrBl divfK ?nz_den // mulrAC -!rmorphM.
 apply: (mulIf (nz_den y)); rewrite mulrAC mulrBl divfK ?nz_den //.
@@ -63,8 +60,23 @@ rewrite !(rmorphM, rmorphB) [_ - _]lock /= -lock !numqE.
 by rewrite (mulrAC y) -!mulrBl -mulrA mulrAC !mulrA.
 Qed.
 
-Canonical char0_ratr_additive  := Additive char0_ratr_is_rmorphism.
-Canonical char0_ratr_rmorphism := RMorphism char0_ratr_is_rmorphism.
+Fact char0_ratr_is_multiplicative : multiplicative ratrF.
+Proof.
+rewrite /char0_ratr.
+have injZtoQ: @injective rat int intr by apply: intr_inj.
+have nz_den x: (denq x)%:~R != 0 :> F by rewrite char0_intr_eq0 // denq_eq0.
+split; rewrite /ratr ?divr1 // => x y.
+rewrite mulrC mulrAC; apply: canLR (mulKf (nz_den _)) _; rewrite !mulrA.
+do 2!apply: canRL (mulfK (nz_den _)) _; rewrite -!rmorphM; congr _%:~R.
+apply: injZtoQ; rewrite !rmorphM [x * y]lock /= !numqE -lock.
+by rewrite -!mulrA mulrA mulrCA -!mulrA (mulrCA y).
+Qed.
+
+HB.instance Definition _ := GRing.isAdditive.Build [zmodType of rat] F ratrF
+  char0_ratr_is_additive.
+HB.instance Definition _ :=
+  GRing.isMultiplicative.Build [ringType of rat] F ratrF
+    char0_ratr_is_multiplicative.
 
 End Char0MorphismsField.
 
diff --git a/theories/xmathcomp/classic_ext.v b/theories/xmathcomp/classic_ext.v
index 21eb643..bdac9db 100644
--- a/theories/xmathcomp/classic_ext.v
+++ b/theories/xmathcomp/classic_ext.v
@@ -1,3 +1,4 @@
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field.
 From Abel Require Import various cyclotomic_ext.
@@ -62,11 +63,15 @@ move=> /irredp_FAdjoin[L1 df [r1 r1_root r1_full]].
 pose L01 := [fieldExtType F0 of baseFieldType L1].
 pose r01 : L01 := r1.
 pose inL01 : L -> L01 := in_alg L1.
-have iota_morph : lrmorphism inL01.
-split; [split; [exact: rmorphB|split; [exact: rmorphM|]]|].
-  by rewrite /inL01 rmorph1.
+have iotam : multiplicative inL01.
+  by split; [exact: rmorphM|rewrite /inL01 rmorph1].
+have iotal : scalable inL01.
   by move=> k a; rewrite /inL01 -mulr_algl rmorphM/= mulr_algl.
-pose iota1 : 'AHom(L, L01) := AHom (linfun_is_ahom (LRMorphism iota_morph)).
+pose iotaaM := GRing.isAdditive.Build _ _ inL01 (rmorphB _).
+pose iotamM := GRing.isMultiplicative.Build _ _ inL01 iotam.
+pose iotalM := GRing.isLinear.Build _ _ _ _ inL01 iotal.
+pose iotaLRM : GRing.LRMorphism.type _ _ := HB.pack inL01 iotaaM iotamM iotalM.
+pose iota1 : 'AHom(L, L01) := AHom (linfun_is_ahom iotaLRM).
 have inL01E : inL01 =1 iota1 by move=> x; rewrite lfunE.
 have r01_root : root (p ^^ iota1) r01 by rewrite -(eq_map_poly inL01E).
 have r01_full : <<limg iota1; r01>>%VS = fullv.
@@ -164,7 +169,9 @@ Proof.
 move=> /(@classic_cycloExt _ L).
 apply/classic_bind => -[M [w [iota wfull wprim]]]; apply/classicW.
 suff splitM : SplittingField.axiom M.
-  by exists (SplittingFieldType F0 M splitM), w, iota.
+  pose mM := FieldExt_isSplittingField.Build F0 M splitM.
+  pose mT : splittingFieldType F0 := HB.pack M mM.
+  by exists mT, w, iota.
 apply: (@SplittingFieldExt _ L ('Phi_n ^^ intr) _ iota).
 rewrite -map_poly_comp (eq_map_poly (rmorph_int _)) -wfull.
 by rewrite (Phi_cyclotomic wprim); apply: splitting_Fadjoin_cyclotomic.
@@ -181,7 +188,9 @@ move=> nN0; suff: classically { L' : fieldExtType F & { w : L' &
   have splitL : SplittingField.axiom L.
     exists (cyclotomic w n); rewrite ?cyclotomic_over// -wfull.
     exact: splitting_Fadjoin_cyclotomic.
-  by exists (SplittingFieldType F L splitL), w.
+  pose lM := FieldExt_isSplittingField.Build F L splitL.
+  pose lT : splittingFieldType F := HB.pack L lM.
+  by exists lT, w.
 pose Fo := [splittingFieldType F of F^o].
 apply: classic_bind (@classic_cycloExt _ Fo n nN0).
 case=> [L [w [iota wfull wprim]]]; apply/classicW.
diff --git a/theories/xmathcomp/map_gal.v b/theories/xmathcomp/map_gal.v
index 0c70e6a..a545e09 100644
--- a/theories/xmathcomp/map_gal.v
+++ b/theories/xmathcomp/map_gal.v
@@ -1,3 +1,4 @@
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field.
 From Abel Require Import various char0.
@@ -49,15 +50,13 @@ apply/trivgP/subsetP=> u uG; rewrite inE.
 by apply/gal_eqP => x xE; rewrite gal_id (fixed_gal _ uG).
 Qed.
 
-Program Canonical prodv_aspace_law :=
-  @Monoid.Law {subfield L} 1%AS (@prodv_aspace _ _) _ _ _.
+Program Definition prodv_aspace_law_mixin :=
+  Monoid.isComLaw.Build {subfield L} 1%AS (@prodv_aspace _ _) _ _ _.
 Next Obligation. by move=> *; apply/val_inj/prodvA. Qed.
+Next Obligation. by move=> *; apply/val_inj/prodvC. Qed.
 Next Obligation. by move=> *; apply/val_inj/prod1v. Qed.
-Next Obligation. by move=> *; apply/val_inj/prodv1. Qed.
 
-Program Canonical prodv_aspace_com_law :=
-  @Monoid.ComLaw {subfield L} 1%AS prodv_aspace_law _.
-Next Obligation. by move=> *; apply/val_inj/prodvC. Qed.
+HB.instance Definition _ := prodv_aspace_law_mixin.
 
 Lemma big_prodv_eq_aspace I (r : seq I) (P : {pred I}) (F : I -> {aspace L}) :
   (\big[@prodv _ _/1%VS]_(i <- r | P i) F i) =
@@ -372,14 +371,20 @@ Proof.
 move=> /= k a b; apply/lfunP => x; rewrite /map_hom.
 by rewrite !(comp_lfunE, add_lfunE, scale_lfunE) linearP.
 Qed.
-Canonical map_hom_linear := Linear map_hom_is_linear.
+HB.instance Definition _ :=
+  GRing.linear_isLinear.Build F0
+    [the lmodType F0 of 'End(L)] [zmodType of 'End(L')] _ map_hom
+    map_hom_is_linear.
 
 Lemma inv_map_hom_is_linear : linear inv_map_hom.
 Proof.
 move=> /= k a b; apply/lfunP => x; rewrite /map_hom.
 by rewrite !(comp_lfunE, add_lfunE, scale_lfunE) linearP.
 Qed.
-Canonical inv_map_hom_linear := Linear inv_map_hom_is_linear.
+HB.instance Definition _ :=
+  GRing.linear_isLinear.Build F0
+    [the lmodType F0 of 'End(L')] [zmodType of 'End(L)] _ inv_map_hom
+    inv_map_hom_is_linear.
 
 Lemma lker0_map_homC (f : 'End(L)) : lker iota == 0%VS ->
   (map_hom f \o iota = iota \o f)%VF.
@@ -523,7 +528,7 @@ Proof. by rewrite !inE map_ahom_kAut. Qed.
 Lemma map_ahom_kEnd_img s : map_ahom s \in kAEnd 1 (iota @: {: L})%AS.
 Proof.
 rewrite inE -(aimg1 iota) map_ahom_kAut// kAutfE.
-exact/kHom_lrmorphism/ahom_is_lrmorphism.
+exact/kHom_lrmorphism/ahom_is_multiplicative.
 Qed.
 
 End map_ahom.
@@ -672,7 +677,7 @@ Implicit Types (K E F : {subfield L}).
 Lemma separable_aimgr E F s : s \in kAEndf E ->
    separable E (s @: F) = separable E F.
 Proof.
-rewrite inE => /kHom_kAut_sub/kAHomP s_id; rewrite -(separable_aimg _ _ s).
+rewrite inE => /kHom_kAut_sub/kAHomP s_id; rewrite -[RHS](separable_aimg _ _ s).
 suff /eq_in_limg->: {in E, s =1 \1%VF} by rewrite lim1g.
 by move=> x xE; rewrite lfunE/= s_id.
 Qed.
@@ -773,7 +778,8 @@ Lemma solvable_ext_refl E : solvable_ext E E.
 Proof.
 by apply/solvable_extP; exists E; rewrite subvv galois_refl/= galvv solvable1.
 Qed.
-Hint Resolve solvable_ext_refl : core.
+Hint Extern 0 (is_true (solvable_ext (asval _) (asval _))) =>
+  (apply: solvable_ext_refl) : core.
 
 Lemma sub_solvable_ext F K E :
   (E <= F)%VS -> solvable_ext K F -> solvable_ext K E.
@@ -837,10 +843,13 @@ Qed.
 
 End normalClosure.
 
-Hint Resolve normalClosureSl : core.
-Hint Resolve normalClosureSr : core.
+Hint Extern 0 (is_true (subsetv (asval _) (normalClosure _ _))) =>
+  (apply: normalClosureSl) : core.
+Hint Extern 0 (is_true (subsetv (asval _) (normalClosure _ _))) =>
+  (apply: normalClosureSr) : core.
 Hint Resolve normalClosure_normal : core.
-Hint Resolve solvable_ext_refl : core.
+Hint Extern 0 (is_true (solvable_ext (asval _) (asval _))) =>
+  (apply: solvable_ext_refl) : core.
 
 Lemma aimg_normalClosure (F0 : fieldType) (L L' : splittingFieldType F0)
   (iota : 'AHom(L, L')) (K E : {subfield L}) :
diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v
index 3138b31..b6602c5 100644
--- a/theories/xmathcomp/various.v
+++ b/theories/xmathcomp/various.v
@@ -1,3 +1,4 @@
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra all_solvable.
 From mathcomp Require Import all_field.
 
@@ -160,11 +161,8 @@ Proof. by move=> x; apply/ffunP => i; rewrite !ffunE mulVg. Qed.
 Lemma extnprod_mulgA : associative extnprod_mulg.
 Proof. by move=> x y z; apply/ffunP => i; rewrite !ffunE mulgA. Qed.
 
-Definition extnprod_groupMixin :=
-  Eval hnf in FinGroup.Mixin extnprod_mulgA extnprod_mul1g extnprod_mulVg.
-Canonical extnprod_baseFinGroupType :=
-  Eval hnf in BaseFinGroupType gTn extnprod_groupMixin.
-Canonical prod_group := FinGroupType extnprod_mulVg.
+HB.instance Definition _ := isMulGroup.Build gTn
+  extnprod_mulgA extnprod_mul1g extnprod_mulVg.
 
 End ExternalNDirProd.
 
@@ -288,9 +286,9 @@ Section ssrnum.
 Import Num.Theory.
 
 Lemma CrealJ (C : numClosedFieldType) :
-  {mono (@conjC C) : x / x \is Num.real}.
+  {mono (@Num.conj_op C) : x / x \is Num.real}.
 Proof.
-suff realK : {homo (@conjC C) : x / x \is Num.real}.
+suff realK : {homo (@Num.conj_op C) : x / x \is Num.real}.
   by move=> x; apply/idP/idP => /realK//; rewrite conjCK.
 by move=> x xreal; rewrite conj_Creal.
 Qed.
@@ -344,12 +342,12 @@ Lemma map_polyXsubC (aR rR : ringType) (f : {rmorphism aR -> rR}) x :
    map_poly f ('X - x%:P) = 'X - (f x)%:P.
 Proof. by rewrite rmorphB/= map_polyX map_polyC. Qed.
 
-Lemma poly_XsubC_over {R : ringType} c (S : {pred R}) (addS : subringPred S)
-  (kS : keyed_pred addS): c \in kS -> 'X - c%:P \is a polyOver kS.
+Lemma poly_XsubC_over {R : ringType} c (S : subringClosed R) :
+  c \in S -> 'X - c%:P \is a polyOver S.
 Proof. by move=> cS; rewrite rpredB ?polyOverC ?polyOverX. Qed.
 
-Lemma poly_XnsubC_over {R : ringType} n c (S : {pred R}) (addS : subringPred S)
-  (kS : keyed_pred addS): c \in kS -> 'X^n - c%:P \is a polyOver kS.
+Lemma poly_XnsubC_over {R : ringType} n c (S : subringClosed R) :
+  c \in S -> 'X^n - c%:P \is a polyOver S.
 Proof. by move=> cS; rewrite rpredB ?rpredX ?polyOverX ?polyOverC. Qed.
 
 Lemma lead_coef_prod {R : idomainType} (ps : seq {poly R}) :
@@ -382,17 +380,17 @@ by rewrite rmorph_prod big_map; apply/eq_bigr => x /=; rewrite map_polyXsubC.
 Qed.
 
 Lemma eq_in_map_poly_id0 (aR rR : ringType) (f g : aR -> rR)
-  (S0 : {pred aR}) (addS : addrPred S0) (kS : keyed_pred addS) :
+    (S : addrClosed aR) :
   f 0 = 0 -> g 0 = 0 ->
-  {in kS, f =1 g} -> {in polyOver kS, map_poly f =1 map_poly g}.
+  {in S, f =1 g} -> {in polyOver S, map_poly f =1 map_poly g}.
 Proof.
 move=> f0 g0 eq_fg p pP; apply/polyP => i.
 by rewrite !coef_map_id0// eq_fg// (polyOverP _).
 Qed.
 
 Lemma eq_in_map_poly (aR rR : ringType) (f g : {additive aR -> rR})
-  (S0 : {pred aR}) (addS : addrPred S0) (kS : keyed_pred addS) :
-  {in kS, f =1 g} -> {in polyOver kS, map_poly f =1 map_poly g}.
+    (S : addrClosed aR) :
+  {in S, f =1 g} -> {in polyOver S, map_poly f =1 map_poly g}.
 Proof. by move=> /eq_in_map_poly_id0; apply; rewrite //?raddf0. Qed.
 
 Lemma mapf_root (F : fieldType) (R : ringType) (f : {rmorphism F -> R})
@@ -727,31 +725,28 @@ Arguments prodv_idPr {F0 L K F}.
 
 Section canonicals.
 Variables  (F0 : fieldType) (L : fieldExtType F0).
-Lemma vsproj_is_lrmorphism :  lrmorphism (vsproj {:L}).
-Proof.
-split; last exact/linearZZ.
-split; first exact/raddfB.
+Lemma vsproj_is_multiplicative : multiplicative (vsproj {:L}).
 by split => [v w|]; apply/val_inj; rewrite /= !vsprojK ?memvf ?algid1.
 Qed.
-Canonical vsproj_lrmorphism := LRMorphism vsproj_is_lrmorphism.
-Canonical vsproj_rmorphism := RMorphism vsproj_is_lrmorphism.
+HB.instance Definition _ :=
+  GRing.isMultiplicative.Build L [ringType of subvs_of {:L}] (vsproj {:L})
+    vsproj_is_multiplicative.
 
 Definition vssub (k K : {vspace L}) of (k <= K)%VS :
   subvs_of k -> subvs_of K := vsproj _ \o vsval.
 
 Variables (k K : {subfield L}) (kK : (k <= K)%VS).
 
-Lemma vssub_is_lrmorphism : lrmorphism (vssub kK).
-split; last exact/linearZZ.
-split; first exact/raddfB.
+Lemma vssub_is_multiplicative : multiplicative (vssub kK).
 split => [v w|]; apply/val_inj => /=; last first.
   by rewrite vsprojK ?algid1 ?rmorph1 ?rpred1//.
 by rewrite /= !vsprojK/= ?rpredM//= (subvP kK _ (subvsP _)) .
 Qed.
-Canonical vssub_additive := Additive vssub_is_lrmorphism.
-Canonical vssub_linear := Linear vssub_is_lrmorphism.
-Canonical vssub_rmorphism := RMorphism vssub_is_lrmorphism.
-Canonical vssub_lrmorphism := LRMorphism vssub_is_lrmorphism.
+HB.instance Definition _ := GRing.Linear.on (vssub kK).
+HB.instance Definition _ :=
+  GRing.isMultiplicative.Build
+    [ringType of subvs_of k] [ringType of subvs_of K] (vssub kK)
+    vssub_is_multiplicative.
 
 Lemma vsval_sub (v : subvs_of k) : vsval (vssub kK v) = vsval v.
 Proof. by rewrite vsprojK// (subvP kK)// subvsP. Qed.
@@ -771,20 +766,29 @@ do [suff init (p : {poly L}) (k : {subfield L})
       {g : 'AHom(L, L') | limg g = E'}] in p *.
   move=> pf pE'; pose K := [FalgType F0 of subvs_of (1%VS : {vspace L})].
   have [idF0 idF0E] : {f : 'AHom(K, L') | forall x : F0, f x%:A = x%:A}.
-    have flr : lrmorphism
-        (fun v : K => in_alg L' (projT1 (sig_eqW (vlineP _ _ (valP v))))).
-      do ![split] => [? ?|? ?||a ?]/=.
-      - case: sig_eqW => x; case: sig_eqW => /= v->; case: sig_eqW => /= w->.
-        by rewrite -!in_algE -raddfB => /fmorph_inj<-//; rewrite raddfB.
+    pose f (v : K) := in_alg L' (projT1 (sig_eqW (vlineP _ _ (valP v)))).
+    have fa : additive f.
+      move=> ? ?; rewrite /f.
+      case: sig_eqW => x; case: sig_eqW => /= v->; case: sig_eqW => /= w->.
+      by rewrite -!in_algE -raddfB => /fmorph_inj<-//; rewrite raddfB.
+    have fm : multiplicative f.
+      split=> [? ?|]; rewrite /f.
       - case: sig_eqW => x; case: sig_eqW => /= v->; case: sig_eqW => /= w->.
         by rewrite -!in_algE -rmorphM => /fmorph_inj<-//; rewrite rmorphM.
       - case: sig_eqW => /= one /esym/eqP; rewrite algid1.
-        by rewrite -in_algE fmorph_eq1 => /eqP->; rewrite scale1r.
-      - case: sig_eqW => x; case: sig_eqW => /= v->.
-        rewrite -mulr_algl -in_algE -rmorphM => /fmorph_inj<-.
-        by rewrite -in_algE rmorphM mulr_algl.
-    exists (linfun_ahom (LRMorphism flr)) => v; rewrite lfunE/=.
-    by case: sig_eqW => /= x; rewrite algid1 -in_algE => /fmorph_inj->.
+        by rewrite -[X in X == _]in_algE fmorph_eq1 => /eqP->; rewrite scale1r.
+    have fl : scalable f.
+      move=> a ? /=; rewrite /f.
+      case: sig_eqW => x; case: sig_eqW => /= v->.
+      rewrite -[_ *: _]mulr_algl -in_algE -rmorphM => /fmorph_inj<-.
+      by rewrite -in_algE rmorphM mulr_algl.
+    pose faM := GRing.isAdditive.Build _ _ _ fa.
+    pose fmM := GRing.isMultiplicative.Build _ _ _ fm.
+    pose flM := GRing.isLinear.Build _ _ _ _ _ fl.
+    pose fLRM : GRing.LRMorphism.type _ _ := HB.pack f faM fmM flM.
+    exists (linfun_ahom fLRM) => v; rewrite lfunE/= /f.
+    case: sig_eqW => /= x.
+    by rewrite algid1 -[in X in X -> _]in_algE => /fmorph_inj->.
   apply: (init (p ^^ in_alg L) 1%AS idF0) => //.
     by apply/polyOver1P; exists p.
   suff -> : limg idF0 = 1%VS.
@@ -887,15 +891,21 @@ have polM (v w : Kx) : pol (val v * val w) = pol (val v) * pol (val w) %% q.
   - by rewrite -ltnS -size_minPoly ltn_modp ?monic_neq0 ?monic_minPoly//.
   rewrite -Fadjoin_poly_mod ?rpredM ?Fadjoin_polyOver//.
   by rewrite hornerM !Fadjoin_poly_eq//= ?rpredM ?subvsP.
-have hlr : lrmorphism (fun v : Kx => (pol (val v) ^^ f).[x']).
-  do ![split] => [v w|v w||w v]/=.
-  - by rewrite -raddfB/= polB raddfB !hornerE.
-  - by rewrite -rmorphM/= polM map_modp/= horner_mod// rmorphM hornerE.
-  - by rewrite algid1 pol1 rmorph1 hornerE.
-  - by rewrite polZ linearZ/= rmorph_alg hornerE mulr_algl.
-pose h := linfun_ahom (LRMorphism hlr).
-exists h; first by rewrite lfunE/= polX map_polyX hornerX.
-by move=> v; rewrite /comp lfunE/= vsval_sub/= polC map_polyC hornerC.
+pose h (v : Kx) := (pol (val v) ^^ f).[x'].
+have ha : additive h.
+  by move=> v w; rewrite /h/= -raddfB/= polB raddfB !hornerE.
+have hm : multiplicative h.
+  split=> [v w|].
+  - by rewrite /h /= -rmorphM/= polM map_modp/= horner_mod// rmorphM hornerE.
+  - by rewrite /h /= algid1 pol1 rmorph1 hornerE.
+have hl : scalable h.
+  by move=> ? ?; rewrite /h /= polZ linearZ/= rmorph_alg hornerE mulr_algl.
+pose haM := GRing.isAdditive.Build _ _ _ ha.
+pose hmM := GRing.isMultiplicative.Build _ _ _ hm.
+pose hlM := GRing.isLinear.Build _ _ _ _ _ hl.
+pose hLRM : GRing.LRMorphism.type _ _ := HB.pack h haM hmM hlM.
+exists (linfun_ahom hLRM); first by rewrite lfunE/= /h polX map_polyX hornerX.
+by move=> v; rewrite /comp lfunE/= /h/= vsval_sub/= polC map_polyC hornerC.
 Qed.
 
 Lemma lker0_img_cap (K : fieldType) (aT rT : vectType K) (f : 'Hom(aT, rT))
@@ -1107,7 +1117,9 @@ Lemma sol_setXn n (gT : 'I_n -> finGroupType) (G : forall i, {group gT i}) :
 Proof.
 elim: n => [|n IHn] in gT G * => solG; first by rewrite setX0 solvable1.
 pose gT' (i : 'I_n) := gT (lift ord0 i).
-pose f (x : prod_group gT) : prod_group gT' := [ffun i => x (lift ord0 i)].
+pose prod_group_gT := [the finGroupType of {dffun forall i, gT i}].
+pose prod_group_gT' := [the finGroupType of {dffun forall i, gT' i}].
+pose f (x : prod_group_gT) : prod_group_gT' := [ffun i => x (lift ord0 i)].
 have fm : morphic (setXn G) f.
   apply/'forall_implyP => -[a b]; rewrite !inE/=.
   by move=> /andP[/forallP aG /forallP bG]; apply/eqP/ffunP => i; rewrite !ffunE.
@@ -1118,8 +1130,8 @@ have -> : (morphm fm @* setXn G)%g = setXn (fun i => G (lift ord0 i)).
     move=> /imsetP[/=x]; rewrite inE => /forallP/= xG ->.
     by move=> i; rewrite morphmE ffunE xG.
   move=> vG; apply/imsetP.
-  pose w : prod_group gT := [ffun i : 'I_n.+1 =>
-             match unliftP ord0 i with
+  pose w := [ffun i : 'I_n.+1 =>
+             match unliftP ord0 i return (gT i) : Type with
              | UnliftSome j i_eq => ecast i (gT i) (esym i_eq) (v j)
              | UnliftNone i0 => 1%g
              end].
@@ -1132,8 +1144,12 @@ have -> : (morphm fm @* setXn G)%g = setXn (fun i => G (lift ord0 i)).
   rewrite inE; apply/forallP => i.
   by case: (unliftP ord0 i) => [j|]->; rewrite ?wl ?w0 ?vG.
 rewrite IHn ?andbT//; last by move=> i; apply: solG.
-pose k (x : gT ord0) : prod_group gT :=
-   [ffun i : 'I_n.+1 => if (ord0 =P i) is ReflectT P then ecast i (gT i) P x else 1%g].
+pose k (x : gT ord0) : prod_group_gT :=
+  [ffun i : 'I_n.+1 =>
+     match (ord0 =P i) return (gT i) : Type with
+     | ReflectT P => ecast i (gT i) P x
+     | _ => 1%g
+     end].
 have km : morphic (G ord0) k.
   apply/'forall_implyP => -[a b]; rewrite !inE/= => /andP[aG bG].
   apply/eqP/ffunP => i; rewrite !ffunE; case: eqP => //; rewrite ?mulg1//.