diff --git a/theories/BGappendixC.v b/theories/BGappendixC.v
index beae551..3913c08 100644
--- a/theories/BGappendixC.v
+++ b/theories/BGappendixC.v
@@ -31,7 +31,7 @@ Let nU := ((p ^ q).-1 %/ p.-1)%N.
 (* External statement of the finite field assumption. *)
 Variant finFieldImage : Prop :=
   FinFieldImage (F : finFieldType) (sigma : {morphism P >-> F}) of
-     isom P [set: F] sigma & sigma @*^-1 <[1 : F]> = P0
+     isom P [set: F] sigma & sigma @*^-1 <[1%R : F]> = P0
    & exists2 sigmaU : {morphism U >-> {unit F}},
      'injm sigmaU & {in P & U, morph_act 'J 'U sigma sigmaU}.
 
diff --git a/theories/PFsection1.v b/theories/PFsection1.v
index 6aae4ac..2a1c2fc 100644
--- a/theories/PFsection1.v
+++ b/theories/PFsection1.v
@@ -35,7 +35,7 @@ Variable gT : finGroupType.
 Lemma odd_eq_conj_irr1 (G : {group gT}) t :
   odd #|G| -> (('chi[G]_t)^*%CF == 'chi_t) = ('chi_t == 1).
 Proof.
-rewrite -coprimen2 => oddG; pose A := <[1 : 'Z_2]>.
+rewrite -coprimen2 => oddG; pose A := <[1%R : 'Z_2]>.
 have Z2P (a : 'Z_2): a = 0 \/ a = 1 by apply/pred2P; case: a => -[|[]].
 pose Ito (t : Iirr G) := [fun a : 'Z_2 => iter a (@conjC_Iirr _ G) t].
 pose Cto (C : {set gT}) := [fun a : 'Z_2 => iter a invg C].