diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v
index 9cbd56e..a324cea 100644
--- a/theories/Core/Semantic/PER/Definitions.v
+++ b/theories/Core/Semantic/PER/Definitions.v
@@ -16,7 +16,7 @@ Notation "R <~> R'" := (relation_equivalence R R') (at level 95, no associativit
 
 Generalizable All Variables.
 
-(** ** Helper Bundles *)
+(** *** Helper Bundles *)
 (** Related modulo evaluation *)
 Inductive rel_mod_eval (R : relation domain -> domain -> domain -> Prop) A ρ A' ρ' R' : Prop := mk_rel_mod_eval : forall a a', {{ ⟦ A ⟧ ρ ↘ a }} -> {{ ⟦ A' ⟧ ρ' ↘ a' }} -> {{ DF a ≈ a' ∈ R ↘ R' }} -> rel_mod_eval R A ρ A' ρ' R'.
 #[global]
@@ -31,7 +31,7 @@ Arguments mk_rel_mod_app {_ _ _ _ _}.
 #[export]
 Hint Constructors rel_mod_app : mcltt.
 
-(** ** (Some Elements of) PER Lattice *)
+(** *** (Some Elements of) PER Lattice *)
 
 Definition per_bot : relation domain_ne := fun m n => (forall s, exists L, {{ Rne m in s ↘ L }} /\ {{ Rne n in s ↘ L }}).
 #[global]
@@ -77,6 +77,7 @@ Inductive per_ne : relation domain :=
 #[export]
 Hint Constructors per_ne : mcltt.
 
+(** * Universe/Element PER *)
 (** ** Universe/Element PER Definition *)
 
 Section Per_univ_elem_core_def.
@@ -229,6 +230,8 @@ End Per_univ_elem_ind_def.
 
 Reserved Notation "'Sub' a <: b 'at' i" (in custom judg at level 90, a custom domain, b custom domain, i constr).
 
+(** * Universe Subtyping *)
+
 Inductive per_subtyp : nat -> domain -> domain -> Prop :=
 | per_subtyp_neut :
   `( {{ Dom b ≈ b' ∈ per_bot }} ->
@@ -255,8 +258,6 @@ where "'Sub' a <: b 'at' i" := (per_subtyp i a b) (in custom judg) : type_scope.
 #[export]
  Hint Constructors per_subtyp : mcltt.
 
-(** ** Context/Environment PER *)
-
 Definition rel_typ i A ρ A' ρ' R' := rel_mod_eval (per_univ_elem i) A ρ A' ρ' R'.
 Arguments rel_typ _ _ _ _ _ _ /.
 #[export]
@@ -264,6 +265,8 @@ Hint Transparent rel_typ : mcltt.
 #[export]
 Hint Unfold rel_typ : mcltt.
 
+(** * Context/Environment PER *)
+
 Inductive per_ctx_env : relation env -> ctx -> ctx -> Prop :=
 | per_ctx_env_nil :
   `{ forall env_rel,
@@ -294,6 +297,8 @@ Hint Unfold valid_ctx : mcltt.
 
 Reserved Notation "'SubE' Γ <: Δ" (in custom judg at level 90, Γ custom exp, Δ custom exp).
 
+(** * Context Subtyping *)
+
 Inductive per_ctx_subtyp : ctx -> ctx -> Prop :=
 | per_ctx_subtyp_nil :
   {{ SubE ⋅ <: ⋅ }}
diff --git a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
index 0f97ba7..4167c67 100644
--- a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
@@ -410,7 +410,7 @@ Ltac apply_predicate_equivalence :=
   rewrite_predicate_equivalence_left;
   clear_predicate_equivalence.
 
-(** ** Simple Morphism instance for [glu_univ_elem] *)
+(** *** Simple Morphism instance for [glu_univ_elem] *)
 Add Parametric Morphism i : (glu_univ_elem i)
     with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> iff as simple_glu_univ_elem_morphism_iff.
 Proof with mautosolve.
@@ -420,7 +420,7 @@ Proof with mautosolve.
     try (etransitivity; [symmetry + idtac|]; eassumption); eauto.
 Qed.
 
-(** ** Morphism instances for [neut_glu_*_pred]s *)
+(** *** Morphism instances for [neut_glu_*_pred]s *)
 Add Parametric Morphism i : (neut_glu_typ_pred i)
     with signature per_bot ==> eq ==> eq ==> iff as neut_glu_typ_pred_morphism_iff.
 Proof with mautosolve.
@@ -450,7 +450,7 @@ Proof with mautosolve.
   split; apply neut_glu_exp_pred_morphism_iff; mauto.
 Qed.
 
-(** ** Morphism instances for [pi_glu_*_pred]s *)
+(** *** Morphism instances for [pi_glu_*_pred]s *)
 Add Parametric Morphism i IR : (pi_glu_typ_pred i IR)
     with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> eq ==> eq ==> iff as pi_glu_typ_pred_morphism_iff.
 Proof with mautosolve.
@@ -662,7 +662,7 @@ Proof.
     eassumption.
 Qed.
 
-(** ** Morphism instances for [glu_univ_elem] *)
+(** *** Morphism instances for [glu_univ_elem] *)
 Add Parametric Morphism i : (glu_univ_elem i)
     with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> per_univ i ==> iff as glu_univ_elem_morphism_iff.
 Proof with mautosolve.
@@ -943,7 +943,7 @@ Proof.
     mauto.
 Qed.
 
-(** ** Simple Morphism instance for [glu_ctx_env] *)
+(** *** Simple Morphism instance for [glu_ctx_env] *)
 Add Parametric Morphism : glu_ctx_env
     with signature glu_sub_pred_equivalence ==> eq ==> iff as simple_glu_ctx_env_morphism_iff.
 Proof.
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 2a69052..eb66d5a 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -565,7 +565,7 @@ Proof.
   eapply glu_univ_elem_exp_lower; mauto.
 Qed.
 
-(** ** Lemmas for [glu_rel_typ_with_sub] and [glu_rel_exp_with_sub] *)
+(** *** Lemmas for [glu_rel_typ_with_sub] and [glu_rel_exp_with_sub] *)
 
 Lemma mk_glu_rel_typ_with_sub' : forall {i Δ A σ ρ a},
     {{ ⟦ A ⟧ ρ ↘ a }} ->
@@ -672,7 +672,7 @@ Qed.
 #[export]
 Hint Resolve glu_rel_typ_with_sub_implies_glu_rel_exp_with_sub : mcltt.
 
-(** ** Lemmas for [glu_ctx_env] *)
+(** *** Lemmas for [glu_ctx_env] *)
 
 Lemma glu_ctx_env_sub_resp_ctx_eq : forall {Γ Sb},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
@@ -1039,7 +1039,7 @@ Proof.
     eapply glu_ctx_env_sub_monotone; mauto 4.
 Qed.
 
-(** ** Tactics for [glu_rel_*] *)
+(** *** Tactics for [glu_rel_*] *)
 
 Ltac destruct_glu_rel_by_assumption sub_glu_rel H :=
   repeat
@@ -1079,7 +1079,7 @@ Ltac destruct_glu_rel_typ_with_sub :=
     end;
   unmark_all.
 
-(** ** Lemmas about [glu_rel_exp] *)
+(** *** Lemmas about [glu_rel_exp] *)
 
 Lemma glu_rel_exp_clean_inversion1 : forall {Γ Sb M A},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
@@ -1148,7 +1148,7 @@ Qed.
 #[export]
 Hint Resolve glu_rel_exp_to_wf_exp : mcltt.
 
-(** ** Lemmas about [glu_rel_sub] *)
+(** *** Lemmas about [glu_rel_sub] *)
 
 Lemma glu_rel_sub_clean_inversion1 : forall {Γ Sb τ Γ'},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
diff --git a/theories/Core/Syntactic/Syntax.v b/theories/Core/Syntactic/Syntax.v
index 908b3bb..aa48764 100644
--- a/theories/Core/Syntactic/Syntax.v
+++ b/theories/Core/Syntactic/Syntax.v
@@ -2,7 +2,7 @@ From Coq Require Import List String.
 
 From Mcltt Require Import Base.
 
-(** ** Concrete Syntax Tree *)
+(** * Concrete Syntax Tree *)
 Module Cst.
 Inductive obj : Set :=
 | typ : nat -> obj
@@ -16,7 +16,7 @@ Inductive obj : Set :=
 | var : string -> obj.
 End Cst.
 
-(** ** Abstract Syntac Tree *)
+(** * Abstract Syntac Tree *)
 Inductive exp : Set :=
 (** Universe *)
 | a_typ : nat -> exp
@@ -65,7 +65,7 @@ Definition exp_to_num e :=
   | None => None
   end.
 
-(** *** Syntactic Normal/Neutral Form *)
+(** ** Syntactic Normal/Neutral Form *)
 Inductive nf : Set :=
 | nf_typ : nat -> nf
 | nf_nat : nf
@@ -123,6 +123,7 @@ Arguments q σ/.
 #[global] Bind Scope mcltt_scope with ne.
 Open Scope mcltt_scope.
 
+(** ** Syntactic Notations *)
 Module Syntax_Notations.
   Notation "{{{ x }}}" := x (at level 0, x custom exp at level 99, format "'{{{'  x  '}}}'") : mcltt_scope.
   Notation "( x )" := x (in custom exp at level 0, x custom exp at level 60) : mcltt_scope.
diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
index 38c2682..2148760 100644
--- a/theories/Core/Syntactic/System/Lemmas.v
+++ b/theories/Core/Syntactic/System/Lemmas.v
@@ -1,7 +1,7 @@
 From Mcltt Require Import Base LibTactics System.Definitions.
 Import Syntax_Notations.
 
-(** ** Core Presuppositions *)
+(** *** Core Presuppositions *)
 Lemma ctx_decomp : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}.
 Proof with now eauto.
   inversion 1...
@@ -220,7 +220,7 @@ Proof with mautosolve.
   assert (m <= max n m) by lia...
 Qed.
 
-(** ** Additional Lemmas for Syntactic PERs *)
+(** *** Additional Lemmas for Syntactic PERs *)
 
 Lemma exp_eq_refl : forall {Γ M A},
     {{ Γ ⊢ M : A }} ->
@@ -251,7 +251,7 @@ Proof. mauto. Qed.
 #[export]
 Hint Resolve sub_eq_refl : mcltt.
 
-(** ** Lemmas for [exp] of [{{{ Type@i }}}] *)
+(** *** Lemmas for [exp] of [{{{ Type@i }}}] *)
 
 Lemma exp_sub_typ : forall {Δ Γ A σ i},
     {{ Δ ⊢ A : Type@i }} ->
@@ -475,7 +475,7 @@ Qed.
 #[export]
 Hint Resolve exp_eq_sub_sub_compose_cong_typ : mcltt.
 
-(** ** Lemmas for [exp] of [{{{ ℕ }}}] *)
+(** *** Lemmas for [exp] of [{{{ ℕ }}}] *)
 
 Lemma exp_sub_nat : forall {Δ Γ M σ},
     {{ Δ ⊢ M : ℕ }} ->
@@ -674,7 +674,7 @@ Qed.
 #[export]
 Hint Resolve exp_eq_sub_sub_compose_cong_nat : mcltt.
 
-(** ** Other Tedious Lemmas *)
+(** *** Other Tedious Lemmas *)
 
 Lemma exp_eq_sub_sub_compose_cong : forall {Γ Δ Δ' Ψ σ τ σ' τ' M A i},
     {{ Ψ ⊢ A : Type@i }} ->
@@ -1018,7 +1018,7 @@ Qed.
 #[export]
 Hint Resolve sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : mcltt.
 
-(** ** Lemmas for [wf_subtyp] *)
+(** *** Lemmas for [wf_subtyp] *)
 
 Fact wf_subtyp_refl : forall {Γ A i},
     {{ Γ ⊢ A : Type@i }} ->
diff --git a/theories/Frontend/Elaborator.v b/theories/Frontend/Elaborator.v
index 56e1e06..0d6c649 100644
--- a/theories/Frontend/Elaborator.v
+++ b/theories/Frontend/Elaborator.v
@@ -209,7 +209,7 @@ Proof.
     assert (y = x); fsetdec.
 Qed.
 
-(** ** Well scopedness lemma *)
+(** *** Well scopedness lemma *)
 
 (** If the set of free variables in a cst are contained in a context
     then elaboration succeeds with that context, and the result is a closed term *)
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index 7224f59..b64b1a4 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -9,14 +9,14 @@ Create HintDb mcltt discriminated.
 #[export]
 Typeclasses Transparent arrows.
 
-(** ** Generalization of Variables *)
+(** *** Generalization of Variables *)
 
 Tactic Notation "gen" ident(x) := generalize dependent x.
 Tactic Notation "gen" ident(x) ident(y) := gen x; gen y.
 Tactic Notation "gen" ident(x) ident(y) ident(z) := gen x y; gen z.
 Tactic Notation "gen" ident(x) ident(y) ident(z) ident(w) := gen x y z; gen w.
 
-(** ** Marking-based Tactics *)
+(** *** Marking-based Tactics *)
 
 Definition __mark__ (n : nat) A (a : A) : A := a.
 Arguments __mark__ n {A} a : simpl never.
@@ -59,7 +59,7 @@ Tactic Notation "on_all_hyp:" tactic4(tac) :=
 Tactic Notation "on_all_hyp_rev:" tactic4(tac) :=
   mark_all_with 0; (on_all_marked_hyp_rev: tac).
 
-(** ** Simple helper *)
+(** *** Simple helper *)
 
 Ltac destruct_logic :=
   destruct_one_pair
@@ -189,7 +189,7 @@ Ltac dir_inversion_clear_by_head head := match_by_head head ltac:(fun H => direc
 Ltac destruct_by_head head := match_by_head head ltac:(fun H => destruct H).
 Ltac dir_destruct_by_head head := match_by_head head ltac:(fun H => directed destruct H).
 
-(** ** McLTT automation *)
+(** *** McLTT automation *)
 
 Tactic Notation "mauto" :=
   eauto with mcltt core.
@@ -403,7 +403,7 @@ Ltac solve_refl :=
       Thus, we try [Equivalence_Reflexive] as well. *)
   solve [reflexivity || apply Equivalence_Reflexive].
 
-(** ** Helper Instances for Generalized Rewriting *)
+(** *** Helper Instances for Generalized Rewriting *)
 #[export]
 Hint Extern 1 (subrelation (@predicate_equivalence ?Ts) _) => (let H := fresh "H" in intros ? ? H; exact H) : typeclass_instances.