diff --git a/theories/nat_cancel.v b/theories/nat_cancel.v
index 97f5437623839f71e2470a061611ea98f0101797..6202dacc96132db780c0a8ebe98ea92e057030a7 100644
--- a/theories/nat_cancel.v
+++ b/theories/nat_cancel.v
@@ -1,6 +1,6 @@
 From stdpp Require Import numbers.
 
-(* The class [NatCancel m n m' n'] is a simple canceler for natural numbers
+(** The class [NatCancel m n m' n'] is a simple canceler for natural numbers
 implemented using type classes.
 
 Input: [m], [n]; output: [m'], [n'].
@@ -71,7 +71,7 @@ Global Instance nat_cancel_leaf_S_else m n m' n' :
   NatCancelLeaf m n m' n' → NatCancelLeaf m (S n) m' (S n') | 4.
 Proof. unfold NatCancelLeaf, NatCancel. omega. Qed.
 
-(* The instance [nat_cancel_S_both] is redundant, but may reduce proof search
+(** The instance [nat_cancel_S_both] is redundant, but may reduce proof search
 quite a bit, e.g. when canceling constants in constants. *)
 Global Instance nat_cancel_S_both m n m' n' :
   NatCancel m n m' n' → NatCancel (S m) (S n) m' n' | 1.
@@ -83,4 +83,4 @@ Proof. unfold NatCancel, MakeNatPlus. omega. Qed.
 Global Instance nat_cancel_S m m' m'' Sm' n n' n'' :
   NatCancel m n m' n' → NatCancelLeaf 1 n' m'' n'' →
   MakeNatS m'' m' Sm' → NatCancel (S m) n Sm' n'' | 3.
-Proof. unfold NatCancelLeaf, NatCancel, MakeNatS. omega. Qed.
\ No newline at end of file
+Proof. unfold NatCancelLeaf, NatCancel, MakeNatS. omega. Qed.