From 53e0f6726824d25a330d52f6fe8c4a98e318f662 Mon Sep 17 00:00:00 2001
From: Jason Hu <fdhzs2010@hotmail.com>
Date: Sun, 15 Sep 2024 19:23:39 -0400
Subject: [PATCH 1/6] exit properly (#209)

---
 driver/Main.ml  | 10 +++++++++-
 driver/Main.mli |  4 ++--
 driver/Mcltt.ml |  5 +++--
 driver/Test.ml  | 28 ++++++++++++++--------------
 4 files changed, 28 insertions(+), 19 deletions(-)

diff --git a/driver/Main.ml b/driver/Main.ml
index 5af280ef..0859dbb5 100644
--- a/driver/Main.ml
+++ b/driver/Main.ml
@@ -4,12 +4,20 @@ open Parser
 open MenhirLibParser.Inter
 open Entrypoint
 
+let get_exit_code result : int =
+  match result with
+  | AllGood _ -> 0
+  | TypeCheckingFailure _ -> 1
+  | ElaborationFailure _ -> 2
+  | ParserFailure _ -> 3
+  | ParserTimeout _ -> 4
+
 let main_of_lexbuf lexbuf =
   Lexer.lexbuf_to_token_buffer lexbuf
   (* Here, the integer argument is a *log* version of fuel.
      Thus, 500 means 2^500. *)
   |> Entrypoint.main 500
-  |> Format.printf "%a@." PrettyPrinter.format_main_result
+  |> fun r -> Format.printf "%a@." PrettyPrinter.format_main_result r; get_exit_code r
 
 let main_of_filename filename =
   Lexing.from_channel (open_in filename) |> main_of_lexbuf
diff --git a/driver/Main.mli b/driver/Main.mli
index 1c724087..44046b52 100644
--- a/driver/Main.mli
+++ b/driver/Main.mli
@@ -1,2 +1,2 @@
-val main_of_filename : string -> unit
-val main_of_program_string : string -> unit
+val main_of_filename : string -> int
+val main_of_program_string : string -> int
diff --git a/driver/Mcltt.ml b/driver/Mcltt.ml
index c6dee3e7..b3ebaa50 100644
--- a/driver/Mcltt.ml
+++ b/driver/Mcltt.ml
@@ -5,7 +5,8 @@ let () =
   then begin
     Printf.fprintf stderr
       "Missing <input-file> argument.\nUsage: %s <input-file>\n" Sys.argv.(0);
-    exit 1
+    exit 5
   end;
   let filename = Sys.argv.(1) in
-  main_of_filename filename
+  let code = main_of_filename filename in
+  exit code
diff --git a/driver/Test.ml b/driver/Test.ml
index 6f36ce61..475cd810 100644
--- a/driver/Test.ml
+++ b/driver/Test.ml
@@ -11,7 +11,7 @@ let main_of_example s = main_of_filename ("../examples/" ^ s)
 (* We never expect parser timeout. 2^500 fuel should be large enough! *)
 
 let%expect_test "Type@0 is of Type@1" =
-  main_of_program_string "Type@0 : Type@1";
+  let _ = main_of_program_string "Type@0 : Type@1" in
   [%expect
     {|
     Parsed:
@@ -23,7 +23,7 @@ let%expect_test "Type@0 is of Type@1" =
   |}]
 
 let%expect_test "zero is of Nat" =
-  main_of_program_string "zero : Nat";
+  let _ = main_of_program_string "zero : Nat" in
   [%expect
     {|
     Parsed:
@@ -35,7 +35,7 @@ let%expect_test "zero is of Nat" =
   |}]
 
 let%expect_test "zero is not of Type@0" =
-  main_of_program_string "zero : Type@0";
+  let _ = main_of_program_string "zero : Type@0" in
   [%expect
     {|
     Type Checking Failure:
@@ -45,7 +45,7 @@ let%expect_test "zero is not of Type@0" =
   |}]
 
 let%expect_test "succ zero is of Nat" =
-  main_of_program_string "succ zero : Nat";
+  let _ = main_of_program_string "succ zero : Nat" in
   [%expect
     {|
     Parsed:
@@ -57,7 +57,7 @@ let%expect_test "succ zero is of Nat" =
   |}]
 
 let%expect_test "succ Type@0 is not of Nat (as it is ill-typed)" =
-  main_of_program_string "succ Type@0 : Nat";
+  let _ = main_of_program_string "succ Type@0 : Nat" in
   [%expect
     {|
     Type Checking Failure:
@@ -67,7 +67,7 @@ let%expect_test "succ Type@0 is not of Nat (as it is ill-typed)" =
   |}]
 
 let%expect_test "variable x is ill-scoped" =
-  main_of_program_string "x : Type@0";
+  let _ = main_of_program_string "x : Type@0" in
   [%expect {|
     Elaboration Failure:
       x
@@ -75,7 +75,7 @@ let%expect_test "variable x is ill-scoped" =
   |}]
 
 let%expect_test "identity function of Nat is of forall (x : Nat) -> Nat" =
-  main_of_program_string "fun (y : Nat) -> y : forall (x : Nat) -> Nat";
+  let _ = main_of_program_string "fun (y : Nat) -> y : forall (x : Nat) -> Nat" in
   [%expect
     {|
     Parsed:
@@ -88,8 +88,8 @@ let%expect_test "identity function of Nat is of forall (x : Nat) -> Nat" =
 
 let%expect_test "recursion on a natural number that always returns zero is of \
                  Nat" =
-  main_of_program_string
-    "rec 3 return y -> Nat | zero => 0 | succ n, r => 0 end : Nat";
+  let _ = main_of_program_string
+    "rec 3 return y -> Nat | zero => 0 | succ n, r => 0 end : Nat" in
   [%expect
     {|
     Parsed:
@@ -101,7 +101,7 @@ let%expect_test "recursion on a natural number that always returns zero is of \
   |}]
 
 let%expect_test "simple_nat.mcl works" =
-  main_of_example "simple_nat.mcl";
+  let _ = main_of_example "simple_nat.mcl" in
   [%expect
     {|
     Parsed:
@@ -113,7 +113,7 @@ let%expect_test "simple_nat.mcl works" =
   |}]
 
 let%expect_test "simple_rec.mcl works" =
-  main_of_example "simple_rec.mcl";
+  let _ = main_of_example "simple_rec.mcl" in
   [%expect
     {|
     Parsed:
@@ -131,7 +131,7 @@ let%expect_test "simple_rec.mcl works" =
   |}]
 
 let%expect_test "pair.mcl works" =
-  main_of_example "pair.mcl";
+  let _ = main_of_example "pair.mcl" in
   [%expect
     {|
     Parsed:
@@ -257,7 +257,7 @@ let%expect_test "pair.mcl works" =
   |}]
 
 let%expect_test "vector.mcl works" =
-  main_of_example "vector.mcl";
+  let _ = main_of_example "vector.mcl" in
   [%expect
     {|
     Parsed:
@@ -465,7 +465,7 @@ let%expect_test "vector.mcl works" =
   |}]
 
 let%expect_test "nary.mcl works" =
-  main_of_example "nary.mcl";
+  let _ = main_of_example "nary.mcl" in
   [%expect
     {|
     Parsed:

From 9e9724adb739e5cd2b6f3aac6a83b28df2cbbae0 Mon Sep 17 00:00:00 2001
From: Jason Hu <fdhzs2010@hotmail.com>
Date: Sun, 15 Sep 2024 23:08:52 -0400
Subject: [PATCH 2/6] [WIP] working on ocaml doc (#191)

* working on ocaml doc

* doesn't include source code at all

* remove opam file
---
 driver/dune           | 2 ++
 driver/extracted/dune | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/driver/dune b/driver/dune
index 9b72c6e2..40e0c90a 100644
--- a/driver/dune
+++ b/driver/dune
@@ -23,3 +23,5 @@
    (:standard -w -67 -w -32 -w -33 -w -39))))
 
 (ocamllex Lexer)
+
+(documentation)
diff --git a/driver/extracted/dune b/driver/extracted/dune
index e535744d..aa468c51 100644
--- a/driver/extracted/dune
+++ b/driver/extracted/dune
@@ -1,3 +1,5 @@
 (library
  (name MclttExtracted)
  (public_name mcltt.extracted))
+
+(documentation)

From 03b83ccec03712d1252c530b2a76d5b7a9226b5f Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Mon, 16 Sep 2024 09:34:33 -0400
Subject: [PATCH 3/6] Update Main.ml (#210)

---
 driver/Main.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/driver/Main.ml b/driver/Main.ml
index 0859dbb5..63a84d71 100644
--- a/driver/Main.ml
+++ b/driver/Main.ml
@@ -7,10 +7,11 @@ open Entrypoint
 let get_exit_code result : int =
   match result with
   | AllGood _ -> 0
-  | TypeCheckingFailure _ -> 1
-  | ElaborationFailure _ -> 2
-  | ParserFailure _ -> 3
-  | ParserTimeout _ -> 4
+  (* 1 and 2 have special meanings in Bash-like shells *)
+  | TypeCheckingFailure _ -> 3
+  | ElaborationFailure _ -> 4
+  | ParserFailure _ -> 5
+  | ParserTimeout _ -> 6
 
 let main_of_lexbuf lexbuf =
   Lexer.lexbuf_to_token_buffer lexbuf

From b42cd1ad390cf2c6ef10c954d04b4183739e1095 Mon Sep 17 00:00:00 2001
From: Jason Hu <fdhzs2010@hotmail.com>
Date: Mon, 16 Sep 2024 10:43:26 -0400
Subject: [PATCH 4/6] Update Mcltt.ml (#211)

avoid exit code clashing
---
 driver/Mcltt.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/driver/Mcltt.ml b/driver/Mcltt.ml
index b3ebaa50..29ca6d20 100644
--- a/driver/Mcltt.ml
+++ b/driver/Mcltt.ml
@@ -5,7 +5,7 @@ let () =
   then begin
     Printf.fprintf stderr
       "Missing <input-file> argument.\nUsage: %s <input-file>\n" Sys.argv.(0);
-    exit 5
+    exit 7
   end;
   let filename = Sys.argv.(1) in
   let code = main_of_filename filename in

From 52b56964c28cc67600f3c3cf3c8fb6ca82a8177e Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Mon, 16 Sep 2024 23:51:27 -0400
Subject: [PATCH 5/6] =?UTF-8?q?Use=20L=C3=B6f=20consistently=20(#212)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 931ff3e2..f3541f3b 100644
--- a/README.md
+++ b/README.md
@@ -2,7 +2,7 @@
 
 In McLTT, we build a verified, runnable typechecker for Martin-Löf type theory. After
 the accomplishment of this project, we will obtain an executable, to which we can feed
-a program in Martin-Loef type theory, and this executable will check whether this
+a program in Martin-Löf type theory, and this executable will check whether this
 program has the specified type. McLTT is novel in that it is implemented in
 Coq. Moreover, we will prove that the typechecking algorithm extracted from Coq is
 sound and complete: a program passes typechecking if and only if it is a well-typed

From 7a0083983e42131f189db5c4148bfab24d566c8a Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Tue, 17 Sep 2024 14:31:53 -0400
Subject: [PATCH 6/6] Update doc comments (#213)

---
 .../Core/Completeness/Consequences/Types.v    | 149 ------------------
 theories/Core/Completeness/FunctionCases.v    |   8 +-
 theories/Core/Completeness/SubtypingCases.v   |   2 +-
 theories/Core/Semantic/PER/Definitions.v      |  20 +--
 theories/Core/Semantic/PER/Lemmas.v           |  20 +--
 theories/Core/Semantic/Readback/Definitions.v |  23 ++-
 theories/Core/Soundness.v                     |   1 -
 .../Soundness/LogicalRelation/CoreLemmas.v    |  10 +-
 .../Soundness/LogicalRelation/Definitions.v   |  19 ++-
 .../Core/Soundness/LogicalRelation/Lemmas.v   |  10 +-
 theories/Core/Soundness/NatCases.v            |   8 +-
 theories/Core/Soundness/Realizability.v       |   8 +-
 theories/Core/Syntactic/CoreInversions.v      |   2 +-
 theories/Core/Syntactic/Corollaries.v         |   6 +-
 theories/Core/Syntactic/CtxSub.v              |  10 +-
 theories/Core/Syntactic/ExpNoConfusion.v      |   2 +-
 theories/Core/Syntactic/Presup.v              |   8 +-
 theories/Core/Syntactic/Syntax.v              |  26 +--
 theories/Core/Syntactic/System/Lemmas.v       |  20 +--
 theories/Extraction/Evaluation.v              |   2 +-
 theories/Extraction/Readback.v                |   2 +-
 theories/Extraction/Subtyping.v               |   5 +-
 theories/Extraction/TypeCheck.v               |  36 ++---
 theories/Frontend/Elaborator.v                |  50 +++---
 theories/LibTactics.v                         |  55 ++++---
 25 files changed, 174 insertions(+), 328 deletions(-)

diff --git a/theories/Core/Completeness/Consequences/Types.v b/theories/Core/Completeness/Consequences/Types.v
index 1ff5058b..63295536 100644
--- a/theories/Core/Completeness/Consequences/Types.v
+++ b/theories/Core/Completeness/Consequences/Types.v
@@ -84,152 +84,3 @@ Qed.
 
 #[export]
 Hint Resolve is_typ_constr_and_exp_eq_nat_implies_eq_nat : mcltt.
-
-(* We cannot use this spec as the definition of [typ_subsumption] as
-   then its transitivity requires [exp_eq_typ_implies_eq_level] or a similar semantic lemma *)
-
-(* Lemma typ_subsumption_spec : forall {Γ A A'}, *)
-(*     {{ Γ ⊢ A ⊆ A' }} -> *)
-(*     {{ ⊢ Γ }} /\ exists j, {{ Γ ⊢ A ≈ A' : Type@j }} \/ exists i i', i < i' /\ {{ Γ ⊢ Type@i ≈ A : Type@j }} /\ {{ Γ ⊢ A' ≈ Type@i' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H. *)
-(*   dependent induction H; split; mauto 3. *)
-(*   - (* typ_subsumption_typ *) *)
-(*     eexists. *)
-(*     right. *)
-(*     do 2 eexists. *)
-(*     repeat split; revgoals; mauto. *)
-(*   - (* typ_subsumption_trans *) *)
-(*     destruct IHtyp_subsumption1 as [? [? [| [i1 [i1']]]]]; destruct IHtyp_subsumption2 as [? [? [| [i2 [i2']]]]]; *)
-(*       destruct_conjs; *)
-(*       only 1: mautosolve 4; *)
-(*       eexists; right; do 2 eexists. *)
-(*     + (* left & right *) *)
-(*       split; [eassumption |]. *)
-(*       solve [mauto using lift_exp_eq_max_left]. *)
-(*     + (* right & left *) *)
-(*       split; [eassumption |]. *)
-(*       solve [mauto using lift_exp_eq_max_right]. *)
-(*     + exvar nat ltac:(fun j => assert {{ Γ ⊢ Type@i2 ≈ Type@i1' : Type@j }} by mauto). *)
-(*       replace i2 with i1' in * by mauto. *)
-(*       split; [etransitivity; revgoals; eassumption |]. *)
-(*       mauto 4 using lift_exp_eq_max_left, lift_exp_eq_max_right. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_spec : mcltt. *)
-
-(* Lemma not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq : forall {Γ A A'}, *)
-(*     is_typ_constr A -> *)
-(*     (forall i, A <> {{{ Type@i }}}) -> *)
-(*     {{ Γ ⊢ A ⊆ A' }} -> *)
-(*     exists j, {{ Γ ⊢ A ≈ A' : Type@j }}. *)
-(* Proof. *)
-(*   intros * ? ? H%typ_subsumption_spec. *)
-(*   destruct_all; mauto. *)
-(*   exfalso. *)
-(*   intuition. *)
-(*   mauto using is_typ_constr_and_exp_eq_typ_implies_eq_typ. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq : mcltt. *)
-
-(* Lemma not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq : forall {Γ A A'}, *)
-(*     is_typ_constr A' -> *)
-(*     (forall i, A' <> {{{ Type@i }}}) -> *)
-(*     {{ Γ ⊢ A ⊆ A' }} -> *)
-(*     exists j, {{ Γ ⊢ A ≈ A' : Type@j }}. *)
-(* Proof. *)
-(*   intros * ? ? H%typ_subsumption_spec. *)
-(*   destruct_all; mauto. *)
-(*   exfalso. *)
-(*   intuition. *)
-(*   mauto using is_typ_constr_and_exp_eq_typ_implies_eq_typ. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq : mcltt. *)
-
-(* Corollary typ_subsumption_left_nat : forall {Γ A'}, *)
-(*     {{ Γ ⊢ ℕ ⊆ A' }} -> *)
-(*     exists j, {{ Γ ⊢ ℕ ≈ A' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H%not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq; mauto. *)
-(*   congruence. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_left_nat : mcltt. *)
-
-(* Corollary typ_subsumption_left_pi : forall {Γ A B C'}, *)
-(*     {{ Γ ⊢ Π A B ⊆ C' }} -> *)
-(*     exists j, {{ Γ ⊢ Π A B ≈ C' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H%not_typ_and_typ_subsumption_left_typ_constr_implies_exp_eq; mauto. *)
-(*   congruence. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_left_pi : mcltt. *)
-
-(* Corollary typ_subsumption_left_typ : forall {Γ i A'}, *)
-(*     {{ Γ ⊢ Type@i ⊆ A' }} -> *)
-(*     exists j i', i <= i' /\ {{ Γ ⊢ A' ≈ Type@i' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H%typ_subsumption_spec. *)
-(*   destruct_all; mauto. *)
-(*   (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst. *)
-(*   mauto using PeanoNat.Nat.lt_le_incl. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_left_typ : mcltt. *)
-
-(* Corollary typ_subsumption_right_nat : forall {Γ A}, *)
-(*     {{ Γ ⊢ A ⊆ ℕ }} -> *)
-(*     exists j, {{ Γ ⊢ A ≈ ℕ : Type@j }}. *)
-(* Proof. *)
-(*   intros * H%not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq; mauto. *)
-(*   congruence. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_right_nat : mcltt. *)
-
-(* Corollary typ_subsumption_right_pi : forall {Γ C A' B'}, *)
-(*     {{ Γ ⊢ C ⊆ Π A' B' }} -> *)
-(*     exists j, {{ Γ ⊢ C ≈ Π A' B' : Type@j }}. *)
-(* Proof. *)
-(*   intros * H%not_typ_and_typ_subsumption_right_typ_constr_implies_exp_eq; mauto. *)
-(*   congruence. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_right_pi : mcltt. *)
-
-(* Corollary typ_subsumption_right_typ : forall {Γ A i'}, *)
-(*     {{ Γ ⊢ A ⊆ Type@i' }} -> *)
-(*     exists j i, i <= i' /\ {{ Γ ⊢ Type@i ≈ A : Type@j }}. *)
-(* Proof. *)
-(*   intros * H%typ_subsumption_spec. *)
-(*   destruct_all; mauto. *)
-(*   (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst. *)
-(*   mauto using PeanoNat.Nat.lt_le_incl. *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_right_typ : mcltt. *)
-
-(* Corollary typ_subsumption_typ_spec : forall {Γ i i'}, *)
-(*     {{ Γ ⊢ Type@i ⊆ Type@i' }} -> *)
-(*     {{ ⊢ Γ }} /\ i <= i'. *)
-(* Proof with mautosolve. *)
-(*   intros * H. *)
-(*   pose proof (typ_subsumption_left_typ H). *)
-(*   destruct_conjs. *)
-(*   (on_all_hyp: fun H => apply exp_eq_typ_implies_eq_level in H); subst... *)
-(* Qed. *)
-
-(* #[export] *)
-(* Hint Resolve typ_subsumption_typ_spec : mcltt. *)
diff --git a/theories/Core/Completeness/FunctionCases.v b/theories/Core/Completeness/FunctionCases.v
index 757729be..0091fefe 100644
--- a/theories/Core/Completeness/FunctionCases.v
+++ b/theories/Core/Completeness/FunctionCases.v
@@ -70,7 +70,7 @@ Lemma rel_exp_pi_core : forall {i o B o' B' R out_rel},
     (forall c c',
         R c c' ->
         rel_exp B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} (per_univ i)) ->
-    (* We use this equality to make unification on `out_rel` works *)
+    (** We use the next equality to make unification on `out_rel` works *)
     (out_rel = fun c c' (equiv_c_c' : R c c') m m' =>
                  forall R',
                    rel_typ i B d{{{ o ↦ c }}} B' d{{{ o' ↦ c' }}} R' ->
@@ -108,8 +108,7 @@ Proof with mautosolve.
   - intros.
     eapply rel_exp_pi_core; eauto.
     reflexivity.
-  - (* `reflexivity` does not work as (simple) unification fails for some unknown reason. *)
-    apply Equivalence_Reflexive.
+  - solve_refl.
 Qed.
 
 #[export]
@@ -140,8 +139,7 @@ Proof with mautosolve.
   - eapply rel_exp_pi_core; eauto; try reflexivity.
     intros.
     extract_output_info_with ρσ c ρ'σ' c' env_relΔA...
-  - (* `reflexivity` does not work as (simple) unification fails for some unknown reason. *)
-    apply Equivalence_Reflexive.
+  - solve_refl.
 Qed.
 
 #[export]
diff --git a/theories/Core/Completeness/SubtypingCases.v b/theories/Core/Completeness/SubtypingCases.v
index df63a3d4..e5015f91 100644
--- a/theories/Core/Completeness/SubtypingCases.v
+++ b/theories/Core/Completeness/SubtypingCases.v
@@ -99,7 +99,7 @@ Proof.
   assert (forall c c', head_rel ρ ρ' equiv_ρ_ρ' c c' -> env_relΓA' d{{{ ρ ↦ c }}} d{{{ ρ' ↦ c' }}}) as HΓA'
       by (intros; apply_relation_equivalence; unshelve eexists; eassumption).
 
-  (* The proofs for the next two assertions are basically the same *)
+  (** The proofs for the next two assertions are basically the same *)
   exvar (relation domain)
     ltac:(fun R => assert ({{ DF Π m0 ρ B ≈ Π m1 ρ' B ∈ per_univ_elem (Nat.max i k) ↘ R }})).
   {
diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v
index 52b9535b..9cbd56e0 100644
--- a/theories/Core/Semantic/PER/Definitions.v
+++ b/theories/Core/Semantic/PER/Definitions.v
@@ -8,30 +8,30 @@ Notation "'Dom' a ≈ b ∈ R" := ((R a b : Prop) : Prop) (in custom judg at lev
 Notation "'DF' a ≈ b ∈ R ↘ R'" := ((R R' a b : Prop) : Prop) (in custom judg at level 90, a custom domain, b custom domain, R constr, R' constr).
 Notation "'Exp' a ≈ b ∈ R" := (R a b : (Prop : Type)) (in custom judg at level 90, a custom exp, b custom exp, R constr).
 Notation "'EF' a ≈ b ∈ R ↘ R'" := (R R' a b : (Prop : Type)) (in custom judg at level 90, a custom exp, b custom exp, R constr, R' constr).
-(* Precedences of the next notations follow the ones in the standard library.
-   However, we do not use the ones in the standard library so that we can change
-   the relation if necessary in the future. *)
+(** Precedences of the next notations follow the ones in the standard library.
+    However, we do not use the ones in the standard library so that we can change
+    the relation if necessary in the future. *)
 Notation "R ~> R'" := (subrelation R R') (at level 70, right associativity).
 Notation "R <~> R'" := (relation_equivalence R R') (at level 95, no associativity).
 
 Generalizable All Variables.
 
-(** Helper Bundles *)
-(* Related modulo evaluation *)
+(** ** 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]
 Arguments mk_rel_mod_eval {_ _ _ _ _ _}.
 #[export]
 Hint Constructors rel_mod_eval : mcltt.
 
-(* Related modulo application *)
+(** Related modulo application *)
 Inductive rel_mod_app f a f' a' (R : relation domain) : Prop := mk_rel_mod_app : forall fa f'a', {{ $| f & a |↘ fa }} -> {{ $| f' & a' |↘ f'a' }} -> {{ Dom fa ≈ f'a' ∈ R }} -> rel_mod_app f a f' a' R.
 #[global]
 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,7 +77,7 @@ Inductive per_ne : relation domain :=
 #[export]
 Hint Constructors per_ne : mcltt.
 
-(** Universe/Element PER Definition *)
+(** ** Universe/Element PER Definition *)
 
 Section Per_univ_elem_core_def.
   Variable
@@ -179,7 +179,7 @@ Qed.
 #[export]
 Hint Resolve per_univ_elem_core_univ' : mcltt.
 
-(** Universe/Element PER Induction Principle *)
+(** ** Universe/Element PER Induction Principle *)
 
 Section Per_univ_elem_ind_def.
   Hypothesis
@@ -255,7 +255,7 @@ 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 *)
+(** ** Context/Environment PER *)
 
 Definition rel_typ i A ρ A' ρ' R' := rel_mod_eval (per_univ_elem i) A ρ A' ρ' R'.
 Arguments rel_typ _ _ _ _ _ _ /.
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index f742ff19..e82cd5e7 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -419,7 +419,7 @@ Ltac do_per_univ_elem_irrel_assert1 :=
       end
   | H1 : {{ DF ~?a ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
       H2 : {{ DF ~_ ≈ ~?a ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
-      (* Order matters less here as H1 and H2 cannot be exchanged *)
+      (** Order matters less here as H1 and H2 cannot be exchanged *)
       assert_fails (unify R1 R2);
       match goal with
       | H : R1 <~> R2 |- _ => fail 1
@@ -451,7 +451,7 @@ Proof with (basic_per_univ_elem_econstructor; mautosolve 4).
     [> split;
      [ intros * HT2; basic_invert_per_univ_elem HT2
      | intros * HTR1 HTR2; apply_relation_equivalence ] ..]; mauto.
-  - (* univ case *)
+  - (** univ case *)
     subst.
     destruct HTR1, HTR2.
     functional_eval_rewrite_clear.
@@ -459,9 +459,9 @@ Proof with (basic_per_univ_elem_econstructor; mautosolve 4).
     eexists.
     specialize (H2 _ _ _ H0) as [].
     intuition.
-  - (* nat case *)
+  - (** nat case *)
     idtac...
-  - (* pi case *)
+  - (** pi case *)
     destruct_conjs.
     basic_per_univ_elem_econstructor; eauto.
     + handle_per_univ_elem_irrel.
@@ -474,7 +474,7 @@ Proof with (basic_per_univ_elem_econstructor; mautosolve 4).
       destruct_rel_mod_eval.
       functional_eval_rewrite_clear.
       handle_per_univ_elem_irrel...
-  - (* fun case *)
+  - (** fun case *)
     intros.
     assert (in_rel c c) by intuition.
     destruct_rel_mod_eval.
@@ -482,7 +482,7 @@ Proof with (basic_per_univ_elem_econstructor; mautosolve 4).
     handle_per_univ_elem_irrel.
     econstructor; eauto.
     intuition.
-  - (* neut case *)
+  - (** neut case *)
     idtac...
 Qed.
 
@@ -539,7 +539,7 @@ Proof.
   - pose proof (fun m0 m1 m2 => per_elem_trans _ _ _ _ m0 m1 m2 H); eauto.
 Qed.
 
-(* This lemma gets rid of the unnecessary PER premise. *)
+(** This lemma gets rid of the unnecessary PER premise. *)
 Lemma per_univ_elem_pi' :
   forall i a a' ρ B ρ' B'
     (in_rel : relation domain)
@@ -909,7 +909,7 @@ Ltac do_per_ctx_env_irrel_assert1 :=
         end
     | H1 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R1 }},
         H2 : {{ DF ~_ ≈ ~?Γ ∈ per_ctx_env ↘ ?R2 }} |- _ =>
-        (* Order matters less here as H1 and H2 cannot be exchanged *)
+        (** Order matters less here as H1 and H2 cannot be exchanged *)
         assert_fails (unify R1 R2);
         match goal with
         | H : R1 <~> R2 |- _ => fail 1
@@ -953,7 +953,7 @@ Proof with solve [eauto using per_univ_trans].
       destruct_rel_typ.
       handle_per_univ_elem_irrel.
       econstructor; intuition.
-      (* This one cannot be replaced with `etransitivity` as we need different `i`s. *)
+      (** This one cannot be replaced with `etransitivity` as we need different `i`s. *)
       eapply per_univ_trans; [| eassumption]; eassumption.
   - destruct_conjs.
     assert (tail_rel d{{{ ρ1 ↯ }}} d{{{ ρ3 ↯ }}}) by eauto.
@@ -999,7 +999,7 @@ Proof.
   - pose proof (fun ρ0 ρ1 ρ2 => per_env_trans _ _ _ ρ0 ρ1 ρ2 H); eauto.
 Qed.
 
-(* This lemma removes the PER argument *)
+(** This lemma removes the PER argument *)
 Lemma per_ctx_env_cons' : forall {Γ Γ' i A A' tail_rel}
                              (head_rel : forall {ρ ρ'} (equiv_ρ_ρ' : {{ Dom ρ ≈ ρ' ∈ tail_rel }}), relation domain)
                              env_rel,
diff --git a/theories/Core/Semantic/Readback/Definitions.v b/theories/Core/Semantic/Readback/Definitions.v
index 77ff2073..27982869 100644
--- a/theories/Core/Semantic/Readback/Definitions.v
+++ b/theories/Core/Semantic/Readback/Definitions.v
@@ -21,10 +21,9 @@ Inductive read_nf : nat -> domain_nf -> nf -> Prop :=
   `( {{ Rne m in s ↘ M }} ->
      {{ Rnf ⇓ ℕ (⇑ ℕ m) in s ↘ ⇑ M }} )
 | read_nf_fn :
-  (* Nf of arg type *)
-  `( {{ Rtyp a in s ↘ A }} ->
-
-     (* Nf of eta-expanded body *)
+  `( (** Normal form of arg type *)
+     {{ Rtyp a in s ↘ A }} ->
+     (** Normal form of eta-expanded body *)
      {{ $| m & ⇑! a s |↘ m' }} ->
      {{ ⟦ B ⟧ ρ ↦ ⇑! a s ↘ b }} ->
      {{ Rnf ⇓ b m' in S s ↘ M }} ->
@@ -42,20 +41,20 @@ with read_ne : nat -> domain_ne -> ne -> Prop :=
      {{ Rnf n in s ↘ N }} ->
      {{ Rne m n in s ↘ M N }} )
 | read_ne_natrec :
-  (* Nf of motive *)
-  `( {{ ⟦ B ⟧ ρ ↦ ⇑! ℕ s ↘ b }} ->
+  `( (** Normal form of motive *)
+     {{ ⟦ B ⟧ ρ ↦ ⇑! ℕ s ↘ b }} ->
      {{ Rtyp b in S s ↘ B' }} ->
 
-     (* Nf of mz *)
+     (** Normal form of mz *)
      {{ ⟦ B ⟧ ρ ↦ zero ↘ bz }} ->
      {{ Rnf ⇓ bz mz in s ↘ MZ }} ->
 
-     (* Nf of MS *)
+     (** Normal form of MS *)
      {{ ⟦ B ⟧ ρ ↦ succ (⇑! ℕ s) ↘ bs }} ->
      {{ ⟦ MS ⟧ ρ ↦ ⇑! ℕ s ↦ ⇑! b (S s) ↘ ms }} ->
      {{ Rnf ⇓ bs ms in S (S s) ↘ MS' }} ->
 
-     (* Ne of m *)
+     (** Neutral form of m *)
      {{ Rne m in s ↘ M }} ->
 
      {{ Rne rec m under ρ return B | zero -> mz | succ -> MS end in s ↘ rec M return B' | zero -> MZ | succ -> MS' end }} )
@@ -66,10 +65,10 @@ with read_typ : nat -> domain -> nf -> Prop :=
 | read_typ_nat :
   `( {{ Rtyp ℕ in s ↘ ℕ }} )
 | read_typ_pi :
-  (* Nf of arg type *)
-  `( {{ Rtyp a in s ↘ A }} ->
+  `( (** Normal form of arg type *)
+     {{ Rtyp a in s ↘ A }} ->
 
-     (* Nf of ret type *)
+     (** Normal form of ret type *)
      {{ ⟦ B ⟧ ρ ↦ ⇑! a s ↘ b }} ->
      {{ Rtyp b in S s ↘ B' }} ->
 
diff --git a/theories/Core/Soundness.v b/theories/Core/Soundness.v
index 4c86d723..6dee1c8d 100644
--- a/theories/Core/Soundness.v
+++ b/theories/Core/Soundness.v
@@ -19,7 +19,6 @@ Proof.
   destruct_conjs.
   functional_initial_env_rewrite_clear.
   assert {{ Γ ⊢s Id ® p ∈ Sb }} by (eapply initial_env_glu_rel_exp; mauto).
-  (* TODO: extract a tactic from this *)
   destruct_glu_rel_exp_with_sub.
   assert {{ Γ ⊢ M[Id] : A[Id] ® m ∈ glu_elem_top i a }} as [] by (eapply realize_glu_elem_top; mauto).
   match_by_head per_top ltac:(fun H => destruct (H (length Γ)) as [W []]).
diff --git a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
index 515bdafa..0f97ba79 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/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v
index 9c512399..2172ea3c 100644
--- a/theories/Core/Soundness/LogicalRelation/Definitions.v
+++ b/theories/Core/Soundness/LogicalRelation/Definitions.v
@@ -13,7 +13,7 @@ Generalizable All Variables.
 Notation "'glu_typ_pred_args'" := (Tcons ctx (Tcons typ Tnil)).
 Notation "'glu_typ_pred'" := (predicate glu_typ_pred_args).
 Notation "'glu_typ_pred_equivalence'" := (@predicate_equivalence glu_typ_pred_args) (only parsing).
-(* This type annotation is to distinguish this notation from others *)
+(** This type annotation is to distinguish this notation from others *)
 Notation "Γ ⊢ A ® R" := ((R Γ A : (Prop : Type)) : (Prop : (Type : Type))) (in custom judg at level 80, Γ custom exp, A custom exp, R constr).
 
 Notation "'glu_exp_pred_args'" := (Tcons ctx (Tcons typ (Tcons exp (Tcons domain Tnil)))).
@@ -61,10 +61,9 @@ Variant neut_glu_exp_pred i a : glu_exp_pred :=
   `{ {{ Γ ⊢ A ® neut_glu_typ_pred i a }} ->
      {{ Γ ⊢ M : A }} ->
      {{ Dom m ≈ m ∈ per_bot }} ->
-     (forall Δ σ (* A' *) M', {{ Δ ⊢w σ : Γ }} ->
-                    (* {{ Rne a in length Δ ↘ A' }} -> *)
-                    {{ Rne m in length Δ ↘ M' }} ->
-                    {{ Δ ⊢ M[σ] ≈ M' : A[σ] }}) ->
+     (forall Δ σ M', {{ Δ ⊢w σ : Γ }} ->
+                   {{ Rne m in length Δ ↘ M' }} ->
+                   {{ Δ ⊢ M[σ] ≈ M' : A[σ] }}) ->
      {{ Γ ⊢ M : A ® ⇑ b m ∈ neut_glu_exp_pred i a }} }.
 
 Variant pi_glu_typ_pred i
@@ -297,17 +296,17 @@ Definition nil_glu_sub_pred : glu_sub_pred :=
   fun Δ σ ρ => {{ Δ ⊢s σ : ⋅ }}.
 Arguments nil_glu_sub_pred Δ σ ρ/.
 
-(* The parameters are ordered differently from the Agda version
-   so that we can return "glu_sub_pred". *)
+(** The parameters are ordered differently from the Agda version
+    so that we can return [glu_sub_pred]. *)
 Variant cons_glu_sub_pred i Γ A (TSb : glu_sub_pred) : glu_sub_pred :=
 | mk_cons_glu_sub_pred :
   `{ forall P El,
         {{ Δ ⊢s σ : Γ, A }} ->
         {{ ⟦ A ⟧ ρ ↯ ↘ a }} ->
         {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
-        (* Here we use [A[Wk][σ]] instead of [A[Wk∘σ]]
-           as syntactic judgement derived from that is
-           a more direct consequence of [{{ Γ, A ⊢ #0 : A[Wk] }}] *)
+        (** Here we use [{{{ A[Wk][σ] }}}] instead of [{{{ A[Wk∘σ] }}}]
+            as syntactic judgement derived from that is
+            a more direct consequence of [{{ Γ, A ⊢ #0 : A[Wk] }}] *)
         {{ Δ ⊢ #0[σ] : A[Wk][σ] ® ~(ρ 0) ∈ El }} ->
         {{ Δ ⊢s Wk ∘ σ ® ρ ↯ ∈ TSb }} ->
         {{ Δ ⊢s σ ® ρ ∈ cons_glu_sub_pred i Γ A TSb }} }.
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index dd432266..2a69052d 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/Soundness/NatCases.v b/theories/Core/Soundness/NatCases.v
index 49919751..a8739802 100644
--- a/theories/Core/Soundness/NatCases.v
+++ b/theories/Core/Soundness/NatCases.v
@@ -437,7 +437,7 @@ Proof.
     invert_rel_typ_body.
     match goal with
     | _: {{ ⟦ A ⟧ ρ ↦ ⇑! ℕ s ↘ ~?a }}, _: {{ ⟦ A ⟧ ρ ↦ (succ ⇑! ℕ s) ↘ ~?a' }} |- _ =>
-        rename a into as'; (* We cannot use [as] as a name *)
+        rename a into as'; (** We cannot use [as] as a name *)
         rename a' into asucc
     end.
     assert {{ Dom ρ ↦ ⇑! ℕ s ↦ ⇑! as' (S s) ≈ ρ ↦ ⇑! ℕ s ↦ ⇑! as' (S s) ∈ env_relΓℕA }} as HΓℕA
@@ -607,11 +607,11 @@ Proof.
     mauto.
   }
   induction 1; intros; rename Γ0 into Δ.
-  - (* glu_nat_zero *)
+  - (** [glu_nat_zero] *)
     mauto 4 using glu_rel_exp_natrec_zero_helper.
-  - (* glu_nat_succ *)
+  - (** [glu_nat_succ] *)
     mauto 3 using glu_rel_exp_natrec_succ_helper.
-  - (* glu_nat_neut *)
+  - (** [glu_nat_neut] *)
     mauto 3 using glu_rel_exp_natrec_neut_helper.
 Qed.
 
diff --git a/theories/Core/Soundness/Realizability.v b/theories/Core/Soundness/Realizability.v
index e5d45e6c..3e18517b 100644
--- a/theories/Core/Soundness/Realizability.v
+++ b/theories/Core/Soundness/Realizability.v
@@ -104,14 +104,14 @@ Theorem realize_glu_univ_elem_gen : forall a i P El,
         {{ Γ ⊢ A ® P }} ->
         {{ Γ ⊢ A ® glu_typ_top i a }}) /\
       (forall Γ M A m,
-          (* We repeat this to get the relation between [a] and [P]
-             more easily after applying [induction 1.] *)
+          (** We repeat this to get the relation between [a] and [P]
+              more easily after applying [induction 1.] *)
           {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
           {{ Γ ⊢ M : A ® m ∈ glu_elem_bot i a }} ->
           {{ Γ ⊢ M : A ® ⇑ a m ∈ El }}) /\
       (forall Γ M A m R,
-          (* We repeat this to get the relation between [a] and [P]
-             more easily after applying [induction 1.] *)
+          (** We repeat this to get the relation between [a] and [P]
+              more easily after applying [induction 1.] *)
           {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
           {{ Γ ⊢ M : A ® m ∈ El }} ->
           {{ DF a ≈ a ∈ per_univ_elem i ↘ R }} ->
diff --git a/theories/Core/Syntactic/CoreInversions.v b/theories/Core/Syntactic/CoreInversions.v
index 2a8e7b57..e4ae9d3e 100644
--- a/theories/Core/Syntactic/CoreInversions.v
+++ b/theories/Core/Syntactic/CoreInversions.v
@@ -103,7 +103,7 @@ Qed.
 #[export]
 Hint Resolve wf_exp_sub_inversion : mcltt.
 
-(* [wf_conv] and [wf_cumu] do not give useful inversions *)
+(** We omit [wf_conv] and [wf_cumu] as they do not give useful inversions *)
 
 Lemma wf_sub_id_inversion : forall Γ Δ,
     {{ Γ ⊢s Id : Δ }} ->
diff --git a/theories/Core/Syntactic/Corollaries.v b/theories/Core/Syntactic/Corollaries.v
index 56fa036a..fd943a9d 100644
--- a/theories/Core/Syntactic/Corollaries.v
+++ b/theories/Core/Syntactic/Corollaries.v
@@ -254,7 +254,7 @@ Qed.
 #[export]
 Hint Resolve exp_eq_natrec_cong_rhs_typ : mcltt.
 
-(* This works for both natrec_sub and app_sub *)
+(** This works for both natrec_sub and app_sub cases *)
 Lemma exp_eq_elim_sub_lhs_typ_gen : forall {Γ σ Δ M A B i},
     {{ Γ ⊢s σ : Δ }} ->
     {{ Δ, A ⊢ B : Type@i }} ->
@@ -273,7 +273,7 @@ Qed.
 #[export]
 Hint Resolve exp_eq_elim_sub_lhs_typ_gen : mcltt.
 
-(* This works for both natrec_sub and app_sub *)
+(** This works for both natrec_sub and app_sub cases *)
 Lemma exp_eq_elim_sub_rhs_typ : forall {Γ σ Δ M A B i},
     {{ Γ ⊢s σ : Δ }} ->
     {{ Δ, A ⊢ B : Type@i }} ->
@@ -386,7 +386,7 @@ Qed.
 #[export]
 Hint Resolve exp_pi_eta_rhs_body : mcltt.
 
-(* This works for both var_0 and var_S *)
+(** This works for both var_0 and var_S cases *)
 Lemma exp_eq_var_sub_rhs_typ_gen : forall {Γ σ Δ i A M},
     {{ Γ ⊢s σ : Δ }} ->
     {{ Δ ⊢ A : Type@i }} ->
diff --git a/theories/Core/Syntactic/CtxSub.v b/theories/Core/Syntactic/CtxSub.v
index a2ab536a..542b23f7 100644
--- a/theories/Core/Syntactic/CtxSub.v
+++ b/theories/Core/Syntactic/CtxSub.v
@@ -39,18 +39,18 @@ Module ctxsub_judg.
       clear ctxsub_exp_helper ctxsub_exp_eq_helper ctxsub_sub_helper ctxsub_sub_eq_helper ctxsub_subtyp_helper;
       intros * HΓΔ; destruct (presup_ctx_sub HΓΔ); mauto 4;
       try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B').
-    (* ctxsub_exp_helper & ctxsub_exp_eq_helper recursion cases *)
+    (** ctxsub_exp_helper & ctxsub_exp_eq_helper recursion cases *)
     1,6-8: assert {{ ⊢ Δ, ℕ ⊆ Γ, ℕ }} by (econstructor; mautosolve);
     assert {{ Δ, ℕ ⊢ B : Type@i }} by eauto; econstructor...
-    (* ctxsub_exp_helper & ctxsub_exp_eq_helper function cases *)
+    (** ctxsub_exp_helper & ctxsub_exp_eq_helper function cases *)
     1-3,5-9: assert {{ Δ ⊢ B : Type@i }} by eauto; assert {{ ⊢ Δ, B ⊆ Γ, B }} by mauto;
     try econstructor...
-    (* ctxsub_exp_helper & ctxsub_exp_eq_helper variable cases *)
+    (** ctxsub_exp_helper & ctxsub_exp_eq_helper variable cases *)
     1-2: assert (exists B, {{ #x : B ∈ Δ }} /\ {{ Δ ⊢ B ⊆ A }}); destruct_conjs; mautosolve 4.
-    (* ctxsub_sub_helper & ctxsub_sub_eq_helper weakening cases *)
+    (** ctxsub_sub_helper & ctxsub_sub_eq_helper weakening cases *)
     2-3: inversion_clear HΓΔ; econstructor; mautosolve 4.
 
-    - (* ctxsub_exp_eq_helper variable case *)
+    - (** ctxsub_exp_eq_helper variable case *)
       inversion_clear HΓΔ as [|Δ0 ? ? C'].
       assert (exists D, {{ #x : D ∈ Δ0 }} /\ {{ Δ0 ⊢ D ⊆ B }}) as [D [i0 ?]] by mauto.
       destruct_conjs.
diff --git a/theories/Core/Syntactic/ExpNoConfusion.v b/theories/Core/Syntactic/ExpNoConfusion.v
index ef598046..23b939af 100644
--- a/theories/Core/Syntactic/ExpNoConfusion.v
+++ b/theories/Core/Syntactic/ExpNoConfusion.v
@@ -1,4 +1,4 @@
-(* For some reason, fitting this file in Syntax.v breaks menhir... Who knows? *)
+(** For some reason, fitting this file in Syntax.v breaks menhir... Who knows? *)
 
 From Equations Require Import Equations.
 From Mcltt Require Import Syntax.
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 6f70f993..4fb4f725 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -63,12 +63,12 @@ Proof with mautosolve 4.
     try (rename M0 into N); try (rename MZ into NZ); try (rename MS into NS);
     try (rename M'0 into N'); try (rename MZ' into NZ'); try (rename MS' into NS');
     try (rename M' into N').
-  (* presup_exp cases *)
+  (** presup_exp cases *)
   - eexists.
     assert {{ Γ ⊢ B : Type@(max i i0) }} by mauto using lift_exp_max_left.
     assert {{ Γ, B ⊢ C : Type@(max i i0) }} by mauto using lift_exp_max_right...
 
-  (* presup_exp_eq cases *)
+  (** presup_exp_eq cases *)
   - assert {{ Γ ⊢s Id ,, N ≈ Id ,, N' : Γ, ℕ }} by mauto 4.
     assert {{ Γ ⊢ B[Id ,, N] ≈ B[Id ,, N'] : Type@i }} by mauto.
     assert {{ Γ ⊢ B[Id ,, N] ≈ B'[Id ,, N'] : Type@i }} by mauto 4.
@@ -254,7 +254,7 @@ Proof with mautosolve 4.
 
   - assert (exists i, {{ Δ ⊢ C : Type@i }}) as []...
 
-  (* presup_sub_eq cases *)
+  (** presup_sub_eq cases *)
   - econstructor...
 
   - assert {{ Γ ⊢ B[σ] ≈ B[σ'] : Type@i }} by mauto 4.
@@ -277,7 +277,7 @@ Proof with mautosolve 4.
     enough {{ Γ ⊢ #0[σ] : A[Wk∘σ] }} by mauto 4.
     eapply wf_conv...
 
-    (* presup_subtyp cases *)
+  (** presup_subtyp cases *)
   - exists (max i i0); split; mauto 3 using lift_exp_max_left, lift_exp_max_right.
   - exists (max (S i) (S j)); split; mauto 3 using lift_exp_max_left, lift_exp_max_right.
   - mauto.
diff --git a/theories/Core/Syntactic/Syntax.v b/theories/Core/Syntactic/Syntax.v
index 826e25b4..908b3bb6 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.
 
-(* CST term *)
+(** ** Concrete Syntax Tree *)
 Module Cst.
 Inductive obj : Set :=
 | typ : nat -> obj
@@ -10,27 +10,28 @@ Inductive obj : Set :=
 | zero : obj
 | succ : obj -> obj
 | natrec : obj -> string -> obj -> obj -> string -> string -> obj -> obj
-| app : obj -> obj -> obj
-| fn : string -> obj -> obj -> obj
 | pi : string -> obj -> obj -> obj
+| fn : string -> obj -> obj -> obj
+| app : obj -> obj -> obj
 | var : string -> obj.
 End Cst.
 
-(* AST term *)
+(** ** Abstract Syntac Tree *)
 Inductive exp : Set :=
-(* Natural numbers *)
+(** Universe *)
+| a_typ : nat -> exp
+(** Natural numbers *)
+| a_nat : exp
 | a_zero : exp
 | a_succ : exp -> exp
 | a_natrec : exp -> exp -> exp -> exp -> exp
-(* Type constructors *)
-| a_nat : exp
-| a_typ : nat -> exp
-| a_var : nat -> exp
-(* Functions *)
+(** Functions *)
+| a_pi : exp -> exp -> exp
 | a_fn : exp -> exp -> exp
 | a_app : exp -> exp -> exp
-| a_pi : exp -> exp -> exp
-(* Substitutions *)
+(** Variable *)
+| a_var : nat -> exp
+(** Substitution Application *)
 | a_sub : exp -> sub -> exp
 with sub : Set :=
 | a_id : sub
@@ -64,6 +65,7 @@ Definition exp_to_num e :=
   | None => None
   end.
 
+(** *** Syntactic Normal/Neutral Form *)
 Inductive nf : Set :=
 | nf_typ : nat -> nf
 | nf_nat : nf
diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v
index ab7e860c..38c2682c 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...
@@ -93,8 +93,8 @@ Qed.
 #[export]
 Hint Resolve presup_exp_eq_ctx : mcltt.
 
-(* Recover some previous rules without subtyping.
-   Rest are recovered after presupposition lemmas (in SystemOpt). *)
+(** Recover some rules we had before adding subtyping.
+    Rest are recovered after presupposition lemmas (in SystemOpt). *)
 
 Lemma wf_ctx_sub_refl : forall Γ Δ,
     {{ ⊢ Γ ≈ Δ }} ->
@@ -106,7 +106,7 @@ Hint Resolve wf_ctx_sub_refl : mcltt.
 
 Lemma wf_conv : forall Γ M A i A',
     {{ Γ ⊢ M : A }} ->
-    (* this will be removed in SystemOpt *)
+    (** The next argument will be removed in SystemOpt *)
     {{ Γ ⊢ A' : Type@i }} ->
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
     {{ Γ ⊢ M : A' }}.
@@ -134,7 +134,7 @@ Hint Resolve wf_sub_conv : mcltt.
 
 Lemma wf_exp_eq_conv : forall Γ M M' A A' i,
    {{ Γ ⊢ M ≈ M' : A }} ->
-    (* this will be removed in SystemOpt *)
+   (** The next argument will be removed in SystemOpt *)
    {{ Γ ⊢ A' : Type@i }} ->
    {{ Γ ⊢ A ≈ A' : Type@i }} ->
    {{ Γ ⊢ M ≈ M' : A' }}.
@@ -220,7 +220,7 @@ Proof with mautosolve.
   assert (m <= max n m) by lia...
 Qed.
 
-(* PER extension *)
+(** ** 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 lemmas *)
+(** ** Other Tedious Lemmas *)
 
 Lemma exp_eq_sub_sub_compose_cong : forall {Γ Δ Δ' Ψ σ τ σ' τ' M A i},
     {{ Ψ ⊢ A : Type@i }} ->
@@ -1018,6 +1018,8 @@ Qed.
 #[export]
 Hint Resolve sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : mcltt.
 
+(** ** Lemmas for [wf_subtyp] *)
+
 Fact wf_subtyp_refl : forall {Γ A i},
     {{ Γ ⊢ A : Type@i }} ->
     {{ Γ ⊢ A ⊆ A }}.
diff --git a/theories/Extraction/Evaluation.v b/theories/Extraction/Evaluation.v
index aecd587b..2f000107 100644
--- a/theories/Extraction/Evaluation.v
+++ b/theories/Extraction/Evaluation.v
@@ -178,7 +178,7 @@ Extraction Inline eval_exp_impl_functional
   eval_app_impl_functional
   eval_sub_impl_functional.
 
-(** The definitions of eval__*_impl already come with soundness proofs,
+(** The definitions of [eval_*_impl] already come with soundness proofs,
     so we only need to prove completeness. However, the completeness
     is also obvious from the soundness of eval orders and functional
     nature of eval. *)
diff --git a/theories/Extraction/Readback.v b/theories/Extraction/Readback.v
index 9eb7bcde..985a6d71 100644
--- a/theories/Extraction/Readback.v
+++ b/theories/Extraction/Readback.v
@@ -165,7 +165,7 @@ Extraction Inline read_nf_impl_functional
   read_ne_impl_functional
   read_typ_impl_functional.
 
-(** The definitions of read__*_impl already come with soundness proofs,
+(** The definitions of [read_*_impl] already come with soundness proofs,
     so we only need to prove completeness. However, the completeness
     is also obvious from the soundness of eval orders and functional
     nature of readback. *)
diff --git a/theories/Extraction/Subtyping.v b/theories/Extraction/Subtyping.v
index 48fc5de7..d0d21b0a 100644
--- a/theories/Extraction/Subtyping.v
+++ b/theories/Extraction/Subtyping.v
@@ -30,8 +30,9 @@ Equations subtyping_nf_impl A B : { {{ ⊢anf A ⊆ B }} } + {~ {{ ⊢anf A ⊆
     let*b _ := nf_eq_dec A A' while _ in
     let*b _ := subtyping_nf_impl B B' while _ in
     pureb _
-(* Pseudo-monadic syntax for the next catch-all branch
-   generates some unsolved obligations *)
+(** Pseudo-monadic syntax for the next catch-all branch
+    generates some unsolved obligations, so we directly match on
+    [nf_eq_dec A B] here. *)
 | A, B with nf_eq_dec A B => {
   | left _ => left _
   | right _ => right _
diff --git a/theories/Extraction/TypeCheck.v b/theories/Extraction/TypeCheck.v
index c203851c..82f2aced 100644
--- a/theories/Extraction/TypeCheck.v
+++ b/theories/Extraction/TypeCheck.v
@@ -213,12 +213,12 @@ Section type_check.
     }
   .
 
-  Next Obligation (* {{ G ⊢a succ M' ⟹ ℕ }} /\ (exists i, {{ G ⊢a ℕ ⟹ Type@i }}) *).
+  Next Obligation. (* {{ G ⊢a succ M' ⟹ ℕ }} /\ (exists i, {{ G ⊢a ℕ ⟹ Type@i }}) *)
     clear_defs.
     mautosolve 4.
   Qed.
 
-  Next Obligation (* exists j, {{ G ⊢ A'[Id,,zero] : Type@j }} *).
+  Next Obligation. (* exists j, {{ G ⊢ A'[Id,,zero] : Type@j }} *)
     clear_defs.
     functional_alg_type_infer_rewrite_clear.
     eexists.
@@ -226,7 +226,7 @@ Section type_check.
     mauto 3.
   Qed.
 
-  Next Obligation (* exists j, {{ G, ℕ, A' ⊢ A'[Wk∘Wk,,succ #1] : Type@i }} *).
+  Next Obligation. (* exists j, {{ G, ℕ, A' ⊢ A'[Wk∘Wk,,succ #1] : Type@i }} *)
     clear_defs.
     functional_alg_type_infer_rewrite_clear.
     eexists.
@@ -234,7 +234,7 @@ Section type_check.
     mauto 3.
   Qed.
 
-  Next Obligation (* nbe_ty_order G {{{ A'[Id,,M'] }}} *).
+  Next Obligation. (* nbe_ty_order G {{{ A'[Id,,M'] }}} *)
     clear_defs.
     enough (exists i, {{ G ⊢ A'[Id,,M'] : ~n{{{ Type@i }}} }}) as [? [? []]%exp_eq_refl%completeness_ty]
         by eauto 3 using nbe_ty_order_sound.
@@ -244,7 +244,7 @@ Section type_check.
     mauto 4 using alg_type_check_sound.
   Qed.
 
-  Next Obligation (* {{ G ⊢a rec M' return A' | zero -> MZ | succ -> MS end ⟹ A'' }} /\ (exists j, {{ G ⊢a A'' ⟹ Type@j }}) *).
+  Next Obligation. (* {{ G ⊢a rec M' return A' | zero -> MZ | succ -> MS end ⟹ A'' }} /\ (exists j, {{ G ⊢a A'' ⟹ Type@j }}) *)
     clear_defs.
     split; [mauto 3 |].
     assert {{ G, ℕ ⊢ A' : ~n{{{ Type@i }}} }} by mauto 4 using alg_type_infer_sound.
@@ -254,18 +254,15 @@ Section type_check.
     assert (exists j, {{ G ⊢a A'' ⟹ Type@j }} /\ j <= i) as [? []] by (gen_presups; mauto 3); firstorder.
   Qed.
 
-  Next Obligation (* nbe_ty_order G A *).
+  Next Obligation. (* {{ ⊢ G, B }} *)
     clear_defs.
-    assert (exists i, {{ G ⊢ A : Type@i }}) as [? [? []]%soundness_ty] by mauto 3.
-    mauto 3 using nbe_ty_order_sound.
+    assert {{ G ⊢ B : Type@i }} by mauto 4 using alg_type_infer_sound.
+    mauto 3.
   Qed.
 
-  Next Obligation. (* {{ G ⊢a #x ⟹ A' }} /\ (exists i, {{ G ⊢a A' ⟹ Type@i }}) *)
+  Next Obligation. (* {{ G ⊢a Π B C ⟹ Type@(max i j) }} /\ (exists k, {{ G ⊢a Type@(max i j) ⟹ Type@k }}) *)
     clear_defs.
-    assert (exists i, {{ G ⊢ A : Type@i }}) as [i] by mauto 3.
-    assert {{ G ⊢ A ≈ A' : Type@i }} by (eapply soundness_ty'; mauto 4 using alg_type_check_sound).
-    assert (user_exp A') by trivial using user_exp_nf.
-    assert (exists j, {{ G ⊢a A' ⟹ Type@j }} /\ j <= i) as [? []] by (gen_presups; mauto 4); firstorder mauto 3.
+    mautosolve 4.
   Qed.
 
   Next Obligation. (* {{ ⊢ G, A' }} *)
@@ -327,15 +324,18 @@ Section type_check.
     firstorder.
   Qed.
 
-  Next Obligation. (* {{ ⊢ G, B }} *)
+  Next Obligation. (* nbe_ty_order G A *)
     clear_defs.
-    assert {{ G ⊢ B : Type@i }} by mauto 4 using alg_type_infer_sound.
-    mauto 3.
+    assert (exists i, {{ G ⊢ A : Type@i }}) as [? [? []]%soundness_ty] by mauto 3.
+    mauto 3 using nbe_ty_order_sound.
   Qed.
 
-  Next Obligation. (* {{ G ⊢a Π B C ⟹ Type@(max i j) }} /\ (exists k, {{ G ⊢a Type@(max i j) ⟹ Type@k }}) *)
+  Next Obligation. (* {{ G ⊢a #x ⟹ A' }} /\ (exists i, {{ G ⊢a A' ⟹ Type@i }}) *)
     clear_defs.
-    mautosolve 4.
+    assert (exists i, {{ G ⊢ A : Type@i }}) as [i] by mauto 3.
+    assert {{ G ⊢ A ≈ A' : Type@i }} by (eapply soundness_ty'; mauto 4 using alg_type_check_sound).
+    assert (user_exp A') by trivial using user_exp_nf.
+    assert (exists j, {{ G ⊢a A' ⟹ Type@j }} /\ j <= i) as [? []] by (gen_presups; mauto 4); firstorder mauto 3.
   Qed.
 
   Extraction Inline type_check_functional type_infer_functional.
diff --git a/theories/Frontend/Elaborator.v b/theories/Frontend/Elaborator.v
index c060068b..56e1e064 100644
--- a/theories/Frontend/Elaborator.v
+++ b/theories/Frontend/Elaborator.v
@@ -8,12 +8,12 @@ Open Scope string_scope.
 Module StrSet := Make String_as_OT.
 Module StrSProp := MSetProperties.Properties StrSet.
 
-(* One cannot import notation from module type without
-   restricting a module to that exact type.
-   Thus here we repeat the notation from WSetsOn. *)
+(** One cannot import notation from module type without
+    restricting a module to that exact type.
+    Thus, here we repeat the notation from [WSetsOn]. *)
 Notation "s [<=] t" := (StrSet.Subset s t) (at level 70, no associativity).
 
-(* De-monadify with pattern matching for now *)
+(** De-monadify with pattern matching for now *)
 Fixpoint lookup (s : string) (ctx : list string) : option nat :=
   match ctx with
   | nil => None
@@ -21,7 +21,7 @@ Fixpoint lookup (s : string) (ctx : list string) : option nat :=
       if string_dec c s
       then Some 0
       else
-        match lookup s cs  with
+        match lookup s cs with
         | Some n => Some (n + 1)%nat
         | None => None
         end
@@ -152,7 +152,7 @@ Inductive closed_at : exp -> nat -> Prop :=
 #[local]
 Hint Constructors closed_at: mcltt.
 
-(*Lemma for the well_scoped proof, lookup succeeds if var is in context*)
+(** Lemma for the well_scoped proof, lookup succeeds if var is in context *)
 Lemma lookup_known (s : string) (ctx : list string) (H_in : List.In s ctx) : exists n : nat, (lookup s ctx = Some n /\ n < List.length ctx).
 Proof.
   induction ctx as [| c ctx' IHctx]; simpl in *.
@@ -165,7 +165,7 @@ Proof.
       eexists; split; auto. lia.
 Qed.
 
-(*Lemma for the well_scoped proof, lookup result always less than context length*)
+(** Lemma for the well_scoped proof, lookup result always less than context length *)
 Lemma lookup_bound s : forall ctx m, lookup s ctx = Some m -> m < (List.length ctx).
   induction ctx.
   - intros. discriminate H.
@@ -209,14 +209,18 @@ Proof.
     assert (y = x); fsetdec.
 Qed.
 
-(*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*)
+(** ** 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 *)
 Lemma well_scoped (cst : Cst.obj) : forall ctx,  cst_variables cst [<=] StrSProp.of_list ctx  ->
 exists a : exp, (elaborate cst ctx = Some a) /\ (closed_at a (List.length ctx)).
 Proof.
   induction cst; intros; simpl in *; mauto.
-  - destruct (IHcst _ H) as [ast [-> ?]]; mauto.
-  - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
+  - (* succ *)
+    destruct (IHcst _ H) as [ast [-> ?]]; mauto.
+  - (* natrec *)
+    assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
     assert (cst_variables cst2 [<=] StrSProp.of_list (s :: ctx)) by (simpl; fsetdec).
     assert (cst_variables cst3 [<=] StrSProp.of_list ctx) by fsetdec.
     assert (cst_variables cst4 [<=] StrSProp.of_list (s1 :: s0 :: ctx)) by (simpl; fsetdec).
@@ -224,16 +228,19 @@ Proof.
       destruct (IHcst2 _ H1) as [ast' [-> ?]];
       destruct (IHcst3 _ H2) as [ast'' [-> ?]];
       destruct (IHcst4 _ H3) as [ast''' [-> ?]]; mauto.
-  - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
-    assert (cst_variables cst2 [<=] StrSProp.of_list ctx) by fsetdec.
+  - (* pi *)
+    assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
+    assert (cst_variables cst2 [<=] StrSProp.of_list (s :: ctx)) by (simpl; fsetdec).
     destruct (IHcst1 _ H0) as [ast [-> ?]];
       destruct (IHcst2 _ H1) as [ast' [-> ?]]; mauto.
-  - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
+  - (* fn *)
+    assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
     assert (cst_variables cst2 [<=] StrSProp.of_list (s :: ctx)) by (simpl; fsetdec).
     destruct (IHcst1 _ H0) as [ast [-> ?]];
       destruct (IHcst2 _ H1) as [ast' [-> ?]]; mauto.
-  - assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
-    assert (cst_variables cst2 [<=] StrSProp.of_list (s :: ctx)) by (simpl; fsetdec).
+  - (* app *)
+    assert (cst_variables cst1 [<=] StrSProp.of_list ctx) by fsetdec.
+    assert (cst_variables cst2 [<=] StrSProp.of_list ctx) by fsetdec.
     destruct (IHcst1 _ H0) as [ast [-> ?]];
       destruct (IHcst2 _ H1) as [ast' [-> ?]]; mauto.
   - apply Subset_to_In in H.
@@ -243,17 +250,6 @@ Proof.
     mauto.
 Qed.
 
-
-(* Check elaborate Cst.nat nil : option exp. *)
-(* Fail Check elaborate (Cst.succ a_nat) : option exp. *)
-
-
-(* Compute (elaborate (Cst.fn "s" (Cst.typ 5) (Cst.var "s")) nil). *)
-(* Compute (elaborate (Cst.fn "s" (Cst.typ 0) (Cst.fn "x" Cst.nat (Cst.app (Cst.var "x") (Cst.var "s")))) nil). *)
-(* Compute (elaborate (Cst.fn "s" Cst.nat (Cst.fn "x" Cst.nat (Cst.fn "s" Cst.nat (Cst.var "s")))) nil). *)
-(* Compute (elaborate (Cst.fn "s" (Cst.typ 10) (Cst.fn "x" (Cst.typ 0) (Cst.fn "s" (Cst.typ 5) (Cst.var "q")))) nil). *)
-
-
 Example test_elab : elaborate Cst.nat nil = Some a_nat.
 Proof. reflexivity. Qed.
 
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index 4944dbf2..7224f597 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -5,18 +5,18 @@ Open Scope predicate_scope.
 
 Create HintDb mcltt discriminated.
 
-(* Transparency setting for generalized rewriting *)
+(** Transparency setting for generalized rewriting *)
 #[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
@@ -113,11 +113,11 @@ Ltac directed tac :=
 Tactic Notation "directed" tactic2(tac) := directed tac.
 
 Ltac progressive_invert H :=
-  (* dependent destruction is more general than inversion *)
+  (** We use dependent destruction as it is more general than inversion *)
   directed dependent destruction H.
 
 #[local]
-  Ltac progressive_invert_once H n :=
+Ltac progressive_invert_once H n :=
   let T := type of H in
   lazymatch T with
   | __mark__ _ _ => fail
@@ -135,7 +135,7 @@ Ltac progressive_invert H :=
   try mark_with H n.
 
 #[global]
-  Ltac progressive_inversion :=
+Ltac progressive_inversion :=
   clear_dups;
   repeat match goal with
     | H : _ |- _ =>
@@ -155,7 +155,7 @@ Ltac clean_replace_by exp0 exp1 tac :=
 Tactic Notation "clean" "replace" uconstr(exp0) "with" uconstr(exp1) "by" tactic3(tac) := clean_replace_by exp0 exp1 tac.
 
 #[global]
-  Ltac find_head t :=
+Ltac find_head t :=
   lazymatch t with
   | ?t' _ => find_head t'
   | _ => t
@@ -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.
@@ -226,7 +226,7 @@ Ltac mautosolve_impl pow := unshelve solve [mauto pow]; solve [constructor].
 Tactic Notation "mautosolve" := mautosolve_impl integer:(5).
 Tactic Notation "mautosolve" int_or_var(pow) := mautosolve_impl pow.
 
-(* Improve type class resolution *)
+(** Improve type class resolution for Equivalence and PER *)
 
 #[export]
 Hint Extern 1 => eassumption : typeclass_instances.
@@ -241,7 +241,7 @@ Hint Extern 1 (@Transitive _ (@predicate_equivalence _)) => simple apply @Equiva
 Hint Extern 1 (@Transitive _ (@predicate_implication _)) => simple apply @PreOrder_Transitive : typeclass_instances.
 
 
-(* intuition tactic default setting *)
+(** Default setting for [intuition] tactic *)
 Ltac Tauto.intuition_solver ::= auto with mcltt core solve_subterm.
 
 Ltac exvar T tac :=
@@ -259,7 +259,7 @@ Ltac exvar T tac :=
         clear x; tac x'
   end.
 
-(* this tactic traverses to the bottom of a lemma following universals and conjunctions to the bottom and apply a tactic *)
+(** this tactic traverses to the bottom of a lemma following universals and conjunctions to the bottom and apply a tactic *)
 Ltac deepexec lem tac :=
   let T := type of lem in
   let T' := eval simpl in T in
@@ -279,7 +279,7 @@ Ltac deepexec lem tac :=
   | _ => tac lem
   end.
 
-(* this tactic is similar to above, but the traversal cuts off when it sees an assumption applicable to a cut-off argument C *)
+(** this tactic is similar to above, but the traversal cuts off when it sees an assumption applicable to a cut-off argument C *)
 Ltac cutexec lem C tac :=
   let CT := type of C in
   let T := type of lem in
@@ -315,15 +315,14 @@ Ltac unify_args H P :=
   end.
 
 #[global]
-  Ltac strong_apply H X :=
+Ltac strong_apply H X :=
   let H' := fresh "H" in
   let T := type of X in
   let R := unify_args H T in
   cutexec R X ltac:(fun L => pose proof (L X) as H'; simpl in H'; clear X; rename H' into X).
 
-
 #[global]
-  Ltac apply_equiv_left1 :=
+Ltac apply_equiv_left1 :=
   let tac1 := fun H R H1 T => (let h := find_head T in unify R h; strong_apply H H1) in
   let tac2 := fun H R G => (let h := find_head G in unify R h; apply H; simpl) in
   match goal with
@@ -333,13 +332,11 @@ Ltac unify_args H P :=
   | H : relation_equivalence ?R _ |- ?G => progress tac2 H R G
   end.
 
-
 #[global]
-  Ltac apply_equiv_left := repeat apply_equiv_left1.
-
+Ltac apply_equiv_left := repeat apply_equiv_left1.
 
 #[global]
-  Ltac apply_equiv_right1 :=
+Ltac apply_equiv_right1 :=
   let tac1 := fun H R H1 T => (let h := find_head T in unify R h; strong_apply H H1) in
   let tac2 := fun H R G => (let h := find_head G in unify R h; apply H; simpl) in
   match goal with
@@ -350,10 +347,10 @@ Ltac unify_args H P :=
   end.
 
 #[global]
-  Ltac apply_equiv_right := repeat apply_equiv_right1.
+Ltac apply_equiv_right := repeat apply_equiv_right1.
 
 #[global]
-  Ltac clear_PER :=
+Ltac clear_PER :=
   repeat match goal with
     | H : PER _ |- _ => clear H
     | H : Symmetric _ |- _ => clear H
@@ -376,7 +373,7 @@ Proof.
 Qed.
 
 #[global]
-  Ltac saturate_refl :=
+Ltac saturate_refl :=
   repeat match goal with
     | H : ?R ?a ?b |- _ =>
         tryif unify a b
@@ -388,7 +385,7 @@ Qed.
     end.
 
 #[global]
-  Ltac saturate_refl_for hd :=
+Ltac saturate_refl_for hd :=
   repeat match goal with
     | H : ?R ?a ?b |- _ =>
         unify_by_head_of R hd;
@@ -401,10 +398,12 @@ Qed.
     end.
 
 #[global]
-  Ltac solve_refl :=
+Ltac solve_refl :=
+  (** Sometimes `reflexivity` does not work as (simple) unification fails for some unknown reason.
+      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.
 
@@ -447,13 +446,13 @@ Proof.
   split; intros []; econstructor; unfold Symmetric, Transitive in *; intuition.
 Qed.
 
-(* The following facility converts search of Proper from type class instances to the local context *)
+(** The following facility converts search of Proper from type class instances to the local context *)
 
 Class PERElem (A : Type) (P : A -> Prop) (R : A -> A -> Prop) :=
   per_elem : forall a, P a -> R a a.
 
 #[export]
-  Instance PERProper (A : Type) (P : A -> Prop) (R : A -> A -> Prop) `(Ins : PERElem A P R) a (H : P a) :
+Instance PERProper (A : Type) (P : A -> Prop) (R : A -> A -> Prop) `(Ins : PERElem A P R) a (H : P a) :
   Proper R a.
 Proof.
   cbv. pose proof per_elem; auto.