diff --git a/auxresults.v b/auxresults.v
index 1208299..fbf7678 100644
--- a/auxresults.v
+++ b/auxresults.v
@@ -1477,8 +1477,6 @@ Proof. by rewrite mulrC modp_mul mulrC. Qed.
 
 End AuxiliaryResults.
 
-Section InjectiveTheory.
-
 Lemma raddf_inj (R S : zmodType) (f : {additive R -> S}) :
    (forall x, f x = 0 -> x = 0) -> injective f.
 Proof.
@@ -1486,7 +1484,9 @@ move=> f_inj x y /eqP; rewrite -subr_eq0 -raddfB => /eqP /f_inj /eqP.
 by rewrite subr_eq0 => /eqP.
 Qed.
 
-(*Variable (R S : ringType) (f : {injmorphism R -> S}).
+(* Section InjectiveTheory.
+
+Variable (R S : ringType) (f : {injmorphism R -> S}).
 
 Lemma rmorph_inj : injective f. Proof. by case: f => [? []]. Qed.
 
@@ -1503,9 +1503,9 @@ by rewrite !coef_map => /rmorph_inj.
 Qed.
 
 Canonical map_poly_is_injective := InjMorphism map_poly_injective.
- *)
+
 End InjectiveTheory.
-(* Hint Resolve rmorph_inj. 
+Hint Resolve rmorph_inj. 
 
 Canonical polyC_is_injective (R : ringType) := InjMorphism (@polyC_inj R).