diff --git a/theories/base.v b/theories/base.v
index 811d46b30e291b2d241168a8c74ed6f47174f72e..4dcc5852a52d0efdc6c17ca691d890f33b803260 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -10,8 +10,8 @@ Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 
-(** Enable implicit generalization. *)
-(* This option enables implicit generalization in arguments of the form
+(** * Enable implicit generalization. *)
+(** This option enables implicit generalization in arguments of the form
    `{...} (i.e., anonymous arguments).  Unfortunately, it also enables
    implicit generalization in `Instance`.  We think that the fact taht both
    behaviors are coupled together is a [bug in
@@ -63,13 +63,13 @@ Class NoBackTrack (P : Prop) := { no_backtrack : P }.
 Hint Extern 0 (NoBackTrack _) => constructor; apply _ : typeclass_instances.
 
 (** * Typeclass opaque definitions *)
-(* The constant [tc_opaque] is used to make definitions opaque for just type
+(** The constant [tc_opaque] is used to make definitions opaque for just type
 class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
 Definition tc_opaque {A} (x : A) : A := x.
 Typeclasses Opaque tc_opaque.
 Arguments tc_opaque {_} _ /.
 
-(* Below we define type class versions of the common logical operators. It is
+(** Below we define type class versions of the common logical operators. It is
 important to note that we duplicate the definitions, and do not declare the
 existing logical operators as type classes. That is, we do not say:
 
diff --git a/theories/tactics.v b/theories/tactics.v
index 56dda3cd78a84c558e70053d4e8458b63d7eb46c..849228769060084f48401cb9b77ef3eeb181635a 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -35,11 +35,10 @@ is rather efficient when having big hint databases, or expensive [Hint Extern]
 declarations as the ones above. *)
 Tactic Notation "intuition" := intuition auto.
 
-(* [done] can get slow as it calls "trivial". [fast_done] can solve way less
-   goals, but it will also always finish quickly.
-   We do 'reflexivity' last because for goals of the form ?x = y, if
-   we have x = y in the context, we will typically want to use the
-   assumption and not reflexivity *)
+(** [done] can get slow as it calls "trivial". [fast_done] can solve way less
+goals, but it will also always finish quickly.  We do 'reflexivity' last because
+for goals of the form ?x = y, if we have x = y in the context, we will typically
+want to use the assumption and not reflexivity *)
 Ltac fast_done :=
   solve
     [ eassumption
@@ -321,7 +320,7 @@ Ltac f_equiv :=
   try simple apply reflexivity.
 Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.
 
-(* The tactic [solve_proper_unfold] unfolds the first head symbol, so that
+(** The tactic [solve_proper_unfold] unfolds the first head symbol, so that
 we proceed by repeatedly using [f_equiv]. *)
 Ltac solve_proper_unfold :=
   (* Try unfolding the head symbol, which is the one we are proving a new property about *)
@@ -335,9 +334,9 @@ Ltac solve_proper_unfold :=
   | |- ?R (?f _ _) (?f _ _) => unfold f
   | |- ?R (?f _) (?f _) => unfold f
   end.
-(* [solve_proper_prepare] does some preparation work before the main
-   [solve_proper] loop.  Having this as a separate tactic is useful for
-   debugging [solve_proper] failure. *)
+(** [solve_proper_prepare] does some preparation work before the main
+[solve_proper] loop.  Having this as a separate tactic is useful for debugging
+[solve_proper] failure. *)
 Ltac solve_proper_prepare :=
   (* Introduce everything *)
   intros;