diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 589e37cb6..5ad88d5ed 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -26,6 +26,9 @@
   
 ### Renamed
 
+- in `exp.v`:
+  + `lnX` -> `lnXn`
+
 ### Generalized
 
 ### Deprecated
diff --git a/theories/Make b/theories/Make
index 4cf4ff2c6..a22b53479 100644
--- a/theories/Make
+++ b/theories/Make
@@ -13,6 +13,7 @@ reals.v
 landau.v
 Rstruct.v
 topology.v
+cantor.v
 prodnormedzmodule.v
 normedtype.v
 realfun.v
diff --git a/theories/cantor.v b/theories/cantor.v
index 1e69e197f..9feff3f38 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -1,8 +1,9 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
-From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum.
-From mathcomp Require Import interval rat fintype finmap.
-Require Import mathcomp_extra boolp classical_sets signed functions cardinality.
-Require Import reals topology.
+From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum interval rat.
+From mathcomp Require Import finmap.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality.
+Require Import reals signed topology.
 From HB Require Import structures.
 
 (******************************************************************************)
diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
index 584635fe3..140acdb08 100644
--- a/theories/constructive_ereal.v
+++ b/theories/constructive_ereal.v
@@ -624,7 +624,7 @@ Context {R : numDomainType}.
 Implicit Type (x : \bar R).
 
 Definition fin_num := [qualify a x : \bar R | (x != -oo) && (x != +oo)].
-Fact fin_num_key : pred_key fin_num. by []. Qed.
+Fact fin_num_key : pred_key fin_num. Proof. by []. Qed.
 Canonical fin_num_keyd := KeyedQualifier fin_num_key.
 
 Lemma fin_numE x : (x \is a fin_num) = (x != -oo) && (x != +oo).
diff --git a/theories/exp.v b/theories/exp.v
index b73775156..ac72b7e26 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -631,7 +631,7 @@ Proof. by move=> x y x_gt0 y_gt0; rewrite -ltr_expR !lnK. Qed.
 Lemma ler_ln : {in Num.pos &, {mono ln : x y / x <= y}}.
 Proof. by move=> x y x_gt0 y_gt0; rewrite -ler_expR !lnK. Qed.
 
-Lemma lnX n x : 0 < x -> ln(x ^+ n) = ln x *+ n.
+Lemma lnXn n x : 0 < x -> ln (x ^+ n) = ln x *+ n.
 Proof.
 move=> x_gt0; elim: n => [|n ih] /=; first by rewrite expr0 ln1 mulr0n.
 by rewrite !exprS lnM ?qualifE//= ?exprn_gt0// mulrS ih.
diff --git a/theories/topology.v b/theories/topology.v
index 33602e38e..823866d2d 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -2520,7 +2520,7 @@ HB.instance Definition _ :=
 
 End Product_Topology.
 
-(** dnbhs *)
+(** deleted neighborhood *)
 
 Definition dnbhs {T : topologicalType} (x : T) :=
   within (fun y => y != x) (nbhs x).