diff --git a/angle.v b/angle.v
index 31a8bfb..3550ba0 100644
--- a/angle.v
+++ b/angle.v
@@ -84,9 +84,11 @@ Abort.
 
 End nthroot.
 
+From mathcomp Require Import reals.
+
 Section angle_def.
 
-Variable T : rcfType.
+Variable T : realType.
 
 Record angle := Angle {
   expi : T[i];
@@ -223,7 +225,7 @@ Arguments pi {T}.
 
 Section angle_basic_prop.
 
-Variable T : rcfType.
+Variable T : realType.
 Implicit Types a b : angle T.
 
 Lemma add_angleE a b : a + b = add_angle a b.
@@ -835,7 +837,7 @@ End angle_basic_prop.
 
 Section half_angle.
 
-Variable T : rcfType.
+Variable T : realType.
 
 Definition half_anglec (x : T[i]) :=
   (if 0 <= complex.Im x then
@@ -1040,7 +1042,7 @@ Qed.
 
 End half_angle.
 
-Lemma atan2_N1N1 (T : rcfType) : atan2 (- 1) (- 1) = - piquarter T *+ 3.
+Lemma atan2_N1N1 (T : realType) : atan2 (- 1) (- 1) = - piquarter T *+ 3.
 Proof.
 rewrite /atan2 ltr0N1 ltrN10 ler0N1 divrr; last first.
   by rewrite unitfE eqr_oppLR oppr0 oner_neq0.
@@ -1050,7 +1052,7 @@ Qed.
 
 Section properties_of_atan2.
 
-Variables (T : rcfType).
+Variables (T : realType).
 
 Lemma sqrtr_sqrN2 (x : T) : x != 0 -> Num.sqrt (x ^- 2) = `|x|^-1.
 Proof.
@@ -1195,7 +1197,7 @@ End properties_of_atan2.
 
 Section derived_trigonometric_functions.
 
-Variable T : rcfType.
+Variable T : realType.
 Implicit Types a : angle T.
 
 Definition cot a := (tan a)^-1.
diff --git a/dh.v b/dh.v
index b00cbe6..33d8613 100644
--- a/dh.v
+++ b/dh.v
@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat poly.
 From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp.
 From mathcomp Require Import realalg complex fingroup perm.
 Require Import ssr_ext angle euclidean skew vec_angle rot frame rigid.
-From mathcomp.analysis Require Import forms.
+From mathcomp.analysis Require Import reals forms.
 
 (******************************************************************************)
 (*                       Denavit-Hartenberg convention                        *)
@@ -149,7 +149,7 @@ End plucker_of_line.
 
 Section denavit_hartenberg_homogeneous_matrix.
 
-Variable T : rcfType.
+Variable T : realType.
 
 Definition dh_mat (jangle : angle T) loffset llength (ltwist : angle T) : 'M[T]_4 :=
   hRx ltwist * hTx llength * hTz loffset * hRz jangle.
@@ -190,7 +190,7 @@ Local Open Scope frame_scope.
 
 Section denavit_hartenberg_convention.
 
-Variable T : rcfType.
+Variable T : realType.
 Variables F0 F1 : tframe T.
 Definition From1To0 := locked (F1 _R^ F0).
 Definition p1_in_0 : 'rV[T]_3 := (\o{F1} - \o{F0}) *m (can_tframe T) _R^ F0.
@@ -444,7 +444,7 @@ End denavit_hartenberg_convention.
 (* TODO: in progress, [angeles] p.141-142 *)
 Module Joint.
 Section joint.
-Variable T : rcfType.
+Variable T : realType.
 Let vector := 'rV[T]_3.
 Record t := mk {
   vaxis : vector ;
@@ -455,7 +455,7 @@ End Joint.
 
 Module Link.
 Section link.
-Variable T : rcfType.
+Variable T : realType.
 Record t := mk {
   length : T ; (* nonnegative, distance between to successive joint axes *)
   offset : T ; (* between to successive X axes *)
@@ -467,7 +467,7 @@ End Link.
 
 Section open_chain.
 
-Variable T : rcfType.
+Variable T : realType.
 Let point := 'rV[T]_3.
 Let vector := 'rV[T]_3.
 Let frame := tframe T.
diff --git a/differential_kinematics.v b/differential_kinematics.v
index d449ea4..f01730a 100644
--- a/differential_kinematics.v
+++ b/differential_kinematics.v
@@ -612,18 +612,18 @@ End derivable_FromTo.
 
 (* the coordinate transformation of a point P1 from frame F1 to frame F
   (eqn 2.33, 3.10) *)
-Definition coortrans (R : rcfType) (F : tframe [ringType of R^o]) (F1 : rframe F)
+Definition coortrans (R : realType) (F : tframe [ringType of R^o]) (F1 : rframe F)
     (P1 : bvec F1) : bvec F :=
   RFrame.o F1 \+b rmap F (FramedVect_of_Bound P1).
 
 (* motion of P1 w.r.t. the fixed frame F (eqn B.2) *)
-Definition motion (R : rcfType) (F : tframe [ringType of R^o]) (F1 : R -> rframe F)
+Definition motion (R : realType) (F : tframe [ringType of R^o]) (F1 : R -> rframe F)
   (P1 : forall t, bvec (F1 t)) t : bvec F := coortrans (P1 t).
 
 (* [sciavicco] p.351-352  *)
 Section kinematics.
 
-Variables (R : rcfType) (F : tframe [ringType of R^o]). (* fixed frame *)
+Variables (R : realType) (F : tframe [ringType of R^o]). (* fixed frame *)
 Variable F1 : R -> rframe F. (* time-varying frame (origin and basis in F) *)
 Hypothesis derivable_F1 : forall t, derivable_mx F1 t 1.
 Hypothesis derivable_F1o : forall t, derivable_mx (@TFrame.o [ringType of R^o] \o F1) t 1.
@@ -728,7 +728,7 @@ End kinematics.
 (* [sciavicco] p.81-82 *)
 Section derivative_of_a_rotation_matrix_contd.
 
-Variables (R : rcfType) (F : tframe [ringType of R^o]).
+Variables (R : realType) (F : tframe [ringType of R^o]).
 Variable F1 : R -> rframe F.
 Hypothesis derivable_F1 : forall t, derivable_mx F1 t 1.
 Variable p1 : forall t, bvec (F1 t).
diff --git a/frame.v b/frame.v
index 12241cb..1035399 100644
--- a/frame.v
+++ b/frame.v
@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat poly.
 From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp.
 From mathcomp Require Import realalg complex fingroup perm.
 Require Import ssr_ext angle euclidean skew vec_angle.
-From mathcomp.analysis Require Import forms.
+From mathcomp.analysis Require Import reals forms.
 
 (******************************************************************************)
 (*                                Frames                                      *)
@@ -90,7 +90,7 @@ Notation "f '|,' i" := (NOFrame.rowframe f i) : frame_scope.
 Local Open Scope frame_scope.
 
 Section non_oriented_frame_properties.
-Variable T : rcfType.
+Variable T : realType.
 Let vector := 'rV[T]_3.
 Implicit Types p : 'rV[T]_3.
 Variable f : noframe T.
@@ -313,7 +313,7 @@ Coercion noframe_of_frame (T : ringType) (f : frame T) : noframe T :=
   Frame.noframe_of f.
 
 Section oriented_frame_properties.
-Variables (T : rcfType) (f : Frame.t T).
+Variables (T : realType) (f : Frame.t T).
 Local Notation "'i'" := (f |, 0).
 Local Notation "'j'" := (f |, 1).
 Local Notation "'k'" := (f |, 2%:R).
@@ -427,7 +427,7 @@ Definition can_tframe := TFrame.mk 0 can_frame.
 
 End canonical_frame.
 
-Lemma basis_change (T : rcfType) (M : 'M[T]_3) (F : noframe T) (A : 'M[T]_3) :
+Lemma basis_change (T : realType) (M : 'M[T]_3) (F : noframe T) (A : 'M[T]_3) :
   let i := F |, 0 in
   let j := F |, 1 in
   let k := F |, 2%:R in
@@ -448,7 +448,7 @@ Qed.
 
 Module Base1.
 Section base1.
-Variables (T : rcfType) (i : 'rV[T]_3).
+Variables (T : realType) (i : 'rV[T]_3).
 Hypothesis normi : norm i = 1.
 Import rv3LieAlgebra.Exports.
 
@@ -501,7 +501,7 @@ Definition frame := Frame.mk is_SO.
 End base1.
 
 Section base1_lemmas.
-Variable T : rcfType.
+Variable T : realType.
 
 (* NB: for information *)
 Lemma je0 : j 'e_0 = 'e_1 :> 'rV[T]_3.
@@ -525,7 +525,7 @@ Qed.
 End base1_lemmas.
 End Base1.
 
-Canonical base1_is_noframe (T : rcfType) (u : 'rV[T]_3) (u1 : norm u = 1) :=
+Canonical base1_is_noframe (T : realType) (u : 'rV[T]_3) (u1 : norm u = 1) :=
   NOFrameInterface.mk u1 (Base1.normj u1) (Base1.normk u1)
   (Base1.idotj u1) (Base1.jdotk u) (Base1.idotk u).
 
@@ -533,7 +533,7 @@ Canonical noframe_subtype (T : rcfType) := [subType for @NOFrame.M T].
 
 Module Base.
 Section build_base.
-Variables (T : rcfType) (u : 'rV[T]_3).
+Variables (T : realType) (u : 'rV[T]_3).
 
 Definition i := if u == 0 then 'e_0 else normalize u.
 Definition j := if u == 0 then 'e_1 else Base1.j i.
@@ -588,7 +588,7 @@ Proof. by rewrite !rowframeE -col_mx3_rowE Frame.MSO. Qed.
 End build_base.
 
 Section build_base_lemmas.
-Variables (T : rcfType) (u : 'rV[T]_3).
+Variables (T : realType) (u : 'rV[T]_3).
 
 Lemma frame0 : frame 0 = can_frame T.
 Proof.
@@ -731,22 +731,22 @@ End build_base_lemmas.
 
 End Base.
 
-Lemma colinear_frame0a (T : rcfType) (u : 'rV[T]_3) : colinear (Base.frame u)|,0 u.
+Lemma colinear_frame0a (T : realType) (u : 'rV[T]_3) : colinear (Base.frame u)|,0 u.
 Proof.
 case/boolP : (u == 0) => [/eqP ->|u0]; first by rewrite colinear0.
 by rewrite -Base.iE /Base.i (negbTE u0) scale_colinear.
 Qed.
 
-Lemma colinear_frame0b (T : rcfType) (u : 'rV[T]_3) : colinear u (Base.frame u)|,0.
+Lemma colinear_frame0b (T : realType) (u : 'rV[T]_3) : colinear u (Base.frame u)|,0.
 Proof. by rewrite colinear_sym colinear_frame0a. Qed.
 
 Definition colinear_frame0 := (colinear_frame0a, colinear_frame0b).
 
-Canonical base_is_noframe (T : rcfType) (u : 'rV[T]_3) :=
+Canonical base_is_noframe (T : realType) (u : 'rV[T]_3) :=
   NOFrameInterface.mk (Base.normi u) (Base.normj u) (Base.normk u)
   (Base.idotj u) (Base.jdotk u) (Base.idotk u).
 
-Canonical frame_is_frame (T : rcfType) (u : 'rV[T]_3) :=
+Canonical frame_is_frame (T : realType) (u : 'rV[T]_3) :=
   @FrameInterface.mk _ (base_is_noframe u) (Base.icrossj u).
 
 (*Module Frame.
@@ -782,7 +782,7 @@ Notation "A _R^ B" := (@FromTo _ A B) : frame_scope.
 
 Section FromTo_properties.
 
-Variable T : rcfType.
+Variable T : realType.
 Implicit Types A B C : frame T.
 
 Lemma FromToE A B : (A _R^ B) = A *m (matrix_of_noframe B)^-1 :> 'M[T]_3.
@@ -833,7 +833,7 @@ Qed.
 End FromTo_properties.
 
 (* TODO: move? *)
-Lemma sqr_norm_frame (T : rcfType) (a : frame T) (v : 'rV[T]_3) :
+Lemma sqr_norm_frame (T : realType) (a : frame T) (v : 'rV[T]_3) :
   norm v ^+ 2 = \sum_(i < 3) (v *d a|,i%:R)^+2.
 Proof.
 have H : norm v = norm (v *m (can_frame T) _R^ a).
@@ -842,10 +842,10 @@ rewrite H sqr_norm [in LHS]sum3E [in RHS]sum3E; congr (_ ^+ 2 + _ ^+ 2 + _ ^+ 2)
   by rewrite FromTo_from_can mxE_dotmul_row_col -tr_row trmxK row_id NOFrame.rowframeE.
 Qed.
 
-Definition noframe_of_FromTo (T : rcfType) (A B : frame T) : noframe T :=
+Definition noframe_of_FromTo (T : realType) (A B : frame T) : noframe T :=
   NOFrame.mk (FromTo_is_O A B).
 
-Definition frame_of_FromTo (T : rcfType) (B A : frame T) : frame T :=
+Definition frame_of_FromTo (T : realType) (B A : frame T) : frame T :=
   @Frame.mk _ (noframe_of_FromTo B A) (FromTo_is_SO B A).
 
 Module FramedVect.
@@ -869,7 +869,7 @@ Proof. by move=> ->. Qed.
 
 Section change_of_coordinate_by_rotation.
 
-Variable T : rcfType.
+Variable T : realType.
 Implicit Types A B : frame T.
 
 Lemma FramedVectvK A (x : fvec A) : `[FramedVect.v x $ A] = x.
@@ -944,7 +944,7 @@ End about_frame.*)
 (* construction of a frame out of three non-colinear points *)
 Module triad.
 Section triad.
-Variable T : rcfType.
+Variable T : realType.
 Let point := 'rV[T]_3.
 
 Variables a b c : point.
@@ -1019,7 +1019,7 @@ End triad.
    trois points de depart et leurs positions d'arrivee
    sample lemma: the rotation obtained behaves like a change of coordinates from left to right *)
 Section transformation_given_three_points.
-Variable T : rcfType.
+Variable T : realType.
 Let vector := 'rV[T]_3.
 Let point := 'rV[T]_3.
 
diff --git a/quaternion.v b/quaternion.v
index a94d732..cdbf920 100644
--- a/quaternion.v
+++ b/quaternion.v
@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat poly.
 From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp.
 From mathcomp Require Import realalg complex fingroup perm.
 Require Import ssr_ext euclidean angle vec_angle frame rot.
-From mathcomp.analysis Require Import forms.
+From mathcomp.analysis Require Import reals forms.
 
 (******************************************************************************)
 (*                            Quaternions                                     *)
@@ -419,7 +419,7 @@ End quaternion.
 Notation "x '^*q'" := (conjq x) : quat_scope.
 
 Section quaternion1.
-Variable R : rcfType.
+Variable R : realType.
 
 Definition sqrq (a : quat R) := a.1 ^+ 2 + norm (a.2) ^+ 2.
 
@@ -769,7 +769,7 @@ End quaternion1.
 Arguments uquat {R}.
 
 Section conjugation.
-Variable R : rcfType.
+Variable R : realType.
 Implicit Types (a : quat R) (v : 'rV[R]_3).
 
 Definition conjugation x v : quat R := x * v%:v * x^*q.
@@ -806,7 +806,7 @@ Qed.
 End conjugation.
 
 Section polar_coordinates.
-Variable R : rcfType.
+Variable R : realType.
 Implicit Types (x : quat R) (v : 'rV[R]_3) (a : angle R).
 
 Definition quat_of_polar a v := mkQuat (cos a) (sin a *: v).
@@ -1154,7 +1154,7 @@ Canonical dual_unitRing := UnitRingType (dual R) dual_UnitRingMixin.
 End dual_number_unit.
 
 Section dual_quaternion.
-Variable R : rcfType (*realType*).
+Variable R : realType.
 Local Open Scope dual_scope.
 
 Definition dquat := @dual (quat_unitRing R).
@@ -1288,7 +1288,7 @@ Notation "x '^*dq'" := (conjdq x) : dual_scope.
 
 (* TODO: dual quaternions and rigid body transformations *)
 Section dquat_rbt.
-Variable R : rcfType (*realType*).
+Variable R : realType.
 Local Open Scope dual_scope.
 Implicit Types x : dquat R.
 
diff --git a/rigid.v b/rigid.v
index 4c0a4c2..ef624e7 100644
--- a/rigid.v
+++ b/rigid.v
@@ -3,6 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat poly.
 From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp.
 From mathcomp Require Import realalg complex finset fingroup perm.
 Require Import ssr_ext angle euclidean skew vec_angle rot frame.
+From mathcomp Require Import reals.
 
 (******************************************************************************)
 (*                         Rigid Body Transformations                         *)
@@ -109,7 +110,7 @@ End central_isometry_n.
 
 Section central_isometry_3.
 
-Variable T : rcfType.
+Variable T : realType.
 Implicit Types f : 'CIso[T]_3.
 
 Local Open Scope frame_scope.
@@ -145,7 +146,7 @@ End central_isometry_3.
 
 Section isometry_3_properties.
 
-Variable T : rcfType.
+Variable T : realType.
 Let vector := 'rV[T]_3.
 Let point := 'rV[T]_3.
 Implicit Types f : 'Iso[T]_3.
@@ -234,7 +235,7 @@ End isometry_3_properties.
 
 Module DIso.
 Section direct_isometry.
-Variable (T : rcfType).
+Variable (T : realType).
 Record t := mk {
   f :> 'Iso[T]_3 ;
   P : iso_sgn f == 1 }.
@@ -247,7 +248,7 @@ Coercion disometry_coercion : DIso.t >-> Iso.t.
 
 Section direct_isometry_3_properties.
 
-Variable T : rcfType.
+Variable T : realType.
 
 Lemma ortho_of_diso_is_SO (f : 'DIso_3[T]) : ortho_of_iso f \is 'SO[T]_3.
 Proof.
@@ -257,7 +258,7 @@ Qed.
 End direct_isometry_3_properties.
 
 Section derivative_map.
-Variable T : rcfType.
+Variable T : realType.
 Let vector := 'rV[T]_3.
 Implicit Types f : 'Iso[T]_3.
 Import rv3LieAlgebra.Exports.
@@ -614,7 +615,7 @@ Proof. by rewrite /hom (det_lblock r) det1 mulr1. Qed.
 
 Section homogeneous_transformations.
 
-Variable T : rcfType.
+Variable T : realType.
 Let homogeneous := 'M[T]_4.
 Implicit Types M : homogeneous.
 Implicit Types r : 'M[T]_3.
@@ -1002,7 +1003,7 @@ move=> ?; rewrite motion_vectorE orth_preserves_norm // rotation_sub //.
 exact: rotP.
 Qed.
 
-Lemma rodrigues_homogeneous (T : rcfType) M u (MSO : M \is 'SO[T]_3) :
+Lemma rodrigues_homogeneous (T : realType) M u (MSO : M \is 'SO[T]_3) :
   axial M != 0 ->
   Aa.angle M != pi ->
   let a := aangle (angle_axis_of_rot M) in
@@ -1062,7 +1063,7 @@ Record object (A : frame) := {
   body : (coor A ^ object_size)%type }.
 *)
 
-Variable T : rcfType.
+Variable T : realType.
 Let point := 'rV[T]_3.
 Implicit Types m : EuclideanMotion.t T.
 
diff --git a/rot.v b/rot.v
index b1b8391..e2962f0 100644
--- a/rot.v
+++ b/rot.v
@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat poly.
 From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp.
 From mathcomp Require Import realalg complex fingroup perm.
 Require Import ssr_ext angle euclidean skew vec_angle frame.
-From mathcomp.analysis Require Import forms.
+From mathcomp.analysis Require Import reals forms.
 
 (******************************************************************************)
 (*                              Rotations                                     *)
@@ -72,7 +72,7 @@ Local Open Scope ring_scope.
 
 Section two_dimensional_rotation.
 
-Variable T : rcfType.
+Variable T : realType.
 Implicit Types (a b : angle T) (M : 'M[T]_2).
 
 Definition RO a := col_mx2 (row2 (cos a) (sin a)) (row2 (- sin a) (cos a)).
@@ -172,7 +172,7 @@ Qed.
 End two_dimensional_rotation.
 
 Section elementary_rotations.
-Variable T : rcfType.
+Variable T : realType.
 Implicit Types a b : angle T.
 
 Local Open Scope frame_scope.
@@ -325,7 +325,7 @@ Section isRot.
 
 Local Open Scope frame_scope.
 
-Variable T : rcfType.
+Variable T : realType.
 Implicit Types a : angle T.
 
 Definition isRot a (u : 'rV[T]_3) (f : {linear 'rV_3 -> 'rV_3}) : bool :=
@@ -569,7 +569,7 @@ End isRot.
 
 Section exponential_map_rot.
 
-Variable T : rcfType.
+Variable T : realType.
 Let vector := 'rV[T]_3.
 Implicit Types (u v w : vector) (a b : angle T) (M : 'M[T]_3).
 
@@ -989,7 +989,7 @@ Notation "'`e^(' a ',' w ')'" := (emx3 a \S( w )).
 Module Aa.
 Section angle_of_angle_axis_representation.
 
-Variable T : rcfType.
+Variable T : realType.
 Let vector := 'rV[T]_3.
 Implicit Types M : 'M[T]_3.
 
@@ -1198,7 +1198,7 @@ End angle_of_angle_axis_representation.
 
 Section axis_of_angle_axis_representation.
 
-Variable T : rcfType.
+Variable T : realType.
 Let vector := 'rV[T]_3.
 
 Definition naxial a (M : 'M[T]_3) := ((sin a) *+ 2)^-1 *: axial M.
@@ -1263,7 +1263,7 @@ End Aa.
 
 Section angle_axis_of_rot.
 
-Variable T : rcfType.
+Variable T : realType.
 Let vector := 'rV[T]_3.
 
 Definition log_rot (M : 'M[T]_3) : angle T * 'rV[T]_3 :=
@@ -1372,7 +1372,7 @@ End angle_axis_of_rot.
 
 Section angle_axis_representation.
 
-Variable T : rcfType.
+Variable T : realType.
 Let vector := 'rV[T]_3.
 
 Record angle_axis := AngleAxis {
@@ -1504,7 +1504,7 @@ End properties_of_orthogonal_matrices.
 
 (* wip *)
 Section euler_angles.
-Variable T : rcfType.
+Variable T : realType.
 Implicit Types R : 'M[T]_3.
 Local Open Scope frame_scope.
 Import rv3LieAlgebra.Exports.
@@ -1827,7 +1827,7 @@ End euler_angles.
 
 Section euler_angles2.
 
-Variables (T : rcfType).
+Variables (T : realType).
 
 (* Nsatz *)
 Lemma Tsth : Setoid_Theory T (@eq T).
diff --git a/screw.v b/screw.v
index f984ff9..0ee4ffa 100644
--- a/screw.v
+++ b/screw.v
@@ -1044,7 +1044,7 @@ End TwistComputationExample.
 
 Module Screw.
 Section screw.
-Variable T : rcfType.
+Variable T : realType.
 Record t := mk {
   l : Line.t T ;
   a : angle T ;
@@ -1306,7 +1306,7 @@ End etwist_alt.
 
 Section Chasles.
 
-Variable T : rcfType.
+Variable T : realType.
 Let vector := 'rV[T]_3.
 Let point := 'rV[T]_3.
 
@@ -1379,7 +1379,7 @@ End Chasles.
 
 Section screw_axis_point_helper.
 
-Variables (T : rcfType) (a : angle T).
+Variables (T : realType) (a : angle T).
 
 Definition Ncos2 := (1 - cos a) *+ 2.
 
@@ -1408,7 +1408,7 @@ End screw_axis_point_helper.
 
 Section screw_axis_point_def.
 
-Variable T : rcfType.
+Variable T : realType.
 Let point := 'rV[T]_3.
 Variable f : 'DIso_3[T].
 Let Q : 'M[T]_3 := ortho_of_iso f.
@@ -1420,7 +1420,7 @@ Definition screw_axis_point (p : point) : point :=
 End screw_axis_point_def.
 
 Section screw_axis_point.
-Variable T : rcfType.
+Variable T : realType.
 Let vector := 'rV[T]_3.
 Let point := 'rV[T]_3.
 Import rv3LieAlgebra.Exports.
@@ -1647,7 +1647,7 @@ End screw_axis_point.
 
 (* [murray] exercise 13, p.77 (wip) *)
 Section twist_coor_trans.
-Variable T : rcfType.
+Variable T : realType.
 Variable s : screw T.
 Let h := Screw.h s.
 Let l := Screw.l s.
diff --git a/vec_angle.v b/vec_angle.v
index f56ff2b..84d0b5b 100644
--- a/vec_angle.v
+++ b/vec_angle.v
@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat poly.
 From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp.
 From mathcomp Require Import realalg complex fingroup perm.
 Require Import ssr_ext angle euclidean.
-From mathcomp.analysis Require Import forms.
+From mathcomp.analysis Require Import reals forms.
 
 (******************************************************************************)
 (*                          Vector angles and lines                           *)
@@ -46,7 +46,7 @@ Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 
 Local Open Scope ring_scope.
 
-Lemma norm1_cossin (T : rcfType) (v : 'rV[T]_2) :
+Lemma norm1_cossin (T : realType) (v : 'rV[T]_2) :
   norm v = 1 -> {a | v``_0 = cos a /\ v``_1 = sin a}.
 Proof.
 move=> v1.
@@ -57,7 +57,7 @@ Qed.
 Import rv3LieAlgebra.Exports.
 
 Section vec_angle.
-Variable T : rcfType.
+Variable T : realType.
 Implicit Types u v : 'rV[T]_3.
 
 Definition vec_angle v w : angle T := arg (v *d w +i* norm (v *v w))%C.
@@ -456,7 +456,7 @@ Qed.
 
 Section colinear1.
 
-Variable T : rcfType.
+Variable T : realType.
 Implicit Types u v : 'rV[T]_3.
 
 Lemma colinear_sin u v (u0 : u != 0) (v0 : v != 0) :
@@ -514,7 +514,7 @@ End colinear1.
 
 Section axial_normal_decomposition.
 
-Variable T : rcfType.
+Variable T : realType.
 Let vector := 'rV[T]_3.
 Implicit Types u v e : vector.
 
@@ -727,7 +727,7 @@ End law_of_sines.
 
 Section law_of_sines1.
 
-Variable T : rcfType.
+Variable T : realType.
 Let point := 'rV[T]_3.
 Let vector := 'rV[T]_3.
 Implicit Types a b c : point.