diff --git a/rocq-demo/rocq_playground.v b/rocq-demo/rocq_playground.v
index ede2f71e..93658709 100644
--- a/rocq-demo/rocq_playground.v
+++ b/rocq-demo/rocq_playground.v
@@ -1,11 +1,11 @@
 (*  SPDX-License-Identifier: LGPL-3.0-or-later
     See Notices.txt for copyright information *)
 
-(*  This file demonstrates converting simple HDL designs into Rocq, as well
+(** This file demonstrates converting simple HDL designs into Rocq, as well
     as proofs by induction that parallels those of formal verification in
     Symbiyosys with the "smtbmc" engine in the "prove" mode. *)
 
-(*  Models a simple register, feeding back to itself. We prove that,
+(** Models a simple register, feeding back to itself. We prove that,
     when initialized to zero, it stays always at zero. *)
 Module simple_register.