diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 9012291..00d2f7a 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -794,6 +794,7 @@ Ltac ring_to_rat :=
           -?[(_ + _)%R]/(_ + _)%Q -?[(_ * _)%R]/(_ * _)%Q
           -?[(- _)%R]/(- _)%Q -?[(_ ^-1)%R]/(_ ^-1)%Q /=.
 
+(*
 Lemma rat_ring_theory : (ring_theory 0%Q 1%Q addq mulq subq oppq eq).
 Proof.
 split => * //; rat_to_ring;
@@ -810,3 +811,4 @@ by move=> p /eqP p_neq0; rat_to_ring; rewrite mulVf.
 Qed.
 
 Add Field rat_field : rat_field_theory.
+*)
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index b346a93..79d0602 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -99,7 +99,7 @@ Lemma ifnzP T n (x y : T) : ifnz_spec n x y (ifnz n x y).
 Proof. by case: n => [|n]; [right | left]. Qed.
 
 (* For pretty-printing. *)
-Definition NumFactor (f : nat * nat) := ([Num of f.1], f.2).
+(* Definition NumFactor (f : nat * nat) := ([Num of f.1], f.2). *)
 
 Definition pfactor p e := p ^ e.
 
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 5091411..6d2d512 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -3,9 +3,11 @@
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
 Require Import ssrfun ssrbool eqtype.
+(*
 Require Import BinNat.
 Require BinPos Ndec.
 Require Export Ring.
+*)
 
 (******************************************************************************)
 (* A version of arithmetic on nat (natural numbers) that is better suited to  *)
@@ -1431,6 +1433,7 @@ End NatTrec.
 
 Notation natTrecE := NatTrec.trecE.
 
+(*
 Lemma eq_binP : Equality.axiom Ndec.Neqb.
 Proof.
 move=> p q; apply: (iffP idP) => [|<-]; last by case: p => //; elim.
@@ -1510,6 +1513,7 @@ by case: b; last (elim=> //= p <-; rewrite natTrecE mulnn -expnM muln2 ?expnS).
 Qed.
 
 End NumberInterpretation.
+*)
 
 (* Big(ger) nat IO; usage:                              *)
 (*     Num 1 072 399                                    *)
@@ -1518,6 +1522,7 @@ End NumberInterpretation.
 (*        to display the resut of an expression that    *)
 (*        returns a larger integer.                     *)
 
+(*
 Record number : Type := Num {bin_of_number :> N}.
 
 Definition extend_number (nn : number) m := Num (nn * 1000 + bin_of_nat m).
@@ -1530,9 +1535,11 @@ Canonical number_eqType := Eval hnf in EqType number number_eqMixin.
 
 Notation "[ 'Num' 'of' e ]" := (Num (bin_of_nat e))
   (at level 0, format "[ 'Num'  'of'  e ]") : nat_scope.
+*)
 
 (* Interface to ring/ring_simplify tactics *)
 
+(*
 Lemma nat_semi_ring : semi_ring_theory 0 1 addn muln (@eq _).
 Proof. exact: mk_srt add0n addnC addnA mul1n mul0n mulnC mulnA mulnDl. Qed.
 
@@ -1544,6 +1551,7 @@ Qed.
 
 Lemma nat_power_theory : power_theory 1 muln (@eq _) nat_of_bin expn.
 Proof. by split; apply: nat_of_exp_bin. Qed.
+*)
 
 (* Interface to the ring tactic machinery. *)
 
@@ -1551,11 +1559,13 @@ Fixpoint pop_succn e := if e is e'.+1 then fun n => pop_succn e' n.+1 else id.
 
 Ltac pop_succn e := eval lazy beta iota delta [pop_succn] in (pop_succn e 1).
 
+(*
 Ltac nat_litteral e :=
   match pop_succn e with
   | ?n.+1 => constr: (bin_of_nat n)
   |     _ => NotConstant
   end.
+*)
 
 Ltac succn_to_add :=
   match goal with
@@ -1568,9 +1578,11 @@ Ltac succn_to_add :=
   | _ => idtac
   end.
 
+(*
 Add Ring nat_ring_ssr : nat_semi_ring (morphism nat_semi_morph,
    constants [nat_litteral], preprocess [succn_to_add],
    power_tac nat_power_theory [nat_litteral]).
+*)
 
 (* A congruence tactic, similar to the boolean one, along with an .+1/+  *)
 (* normalization tactic.                                                 *)