diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 8057d97f1b435aac64b3248e416a63cfd432f15c..01f305780a99ae4f6fba2f60f8aae67c0263702c 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -93,7 +93,7 @@ Notation "'letcall:' x := f args 'in' e" :=
   (letcont: "_k" [ x ] := e in call: f args → "_k")%E
   (at level 102, x, f, args at level 1, e at level 150) : expr_scope.
 
-(* RJ: These notations unfortunately do not print.  Also, I don't think
+(* These notations unfortunately do not print.  Also, I don't think
    we would even want them to print in general.
    TODO: Introduce a Definition. *)
 Notation "e1 '<-{Σ' i } '()'" := (e1 <- #i)%E
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 3321b135b6fd5cecc7a04f3c988545d9539c9a83..647f112b95a7e8cd4c6d5829cd8c5e361852b21a 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -118,7 +118,7 @@ Lemma next_access_head_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' a1 a2 l :
 Proof.
   intros Ha1 Hstep Ha2. inversion Ha1; subst; clear Ha1; inv_head_step;
   destruct Ha2; simplify_eq; econstructor; eauto; try apply lookup_insert.
-  (* Oh my. FIXME RJ. *)
+  (* Oh my. FIXME. *)
   - eapply lit_neq_state; last done.
     setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
     cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 41e689c18c8c36cde0c571247ab180fa16260e25..5f77eea264f6416e2bf28b5377e72d86789894f2 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -498,8 +498,6 @@ Proof.
   iApply ("Hvs" $! I'' with "Hinv HPb H†").
 Qed.
 
-(* TODO RJ: Are there still places where this lemma
-   is re-proven inline? *)
 Lemma lft_vs_cons κ Pb Pb' Pi :
   (lft_bor_dead κ -∗ ▷ Pb'-∗ [†κ] ={↑borN}=∗ lft_bor_dead κ ∗ ▷ Pb) -∗
   lft_vs κ Pb Pi -∗ lft_vs κ Pb' Pi.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 58e80365813c476c5d6e719d34785630c9951666..e596aca90194bf294feed5389c3d3c12cb1a559f 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -49,7 +49,7 @@ Section refcell_functions.
     funrec: <> ["x"] :=
       let: "r" := new [ #ty.(ty_size)] in
       "r" <-{ty.(ty_size)} !("x" +ₗ #1);;
-          (* TODO RJ: Can we make it so that the parenthesis above are mandatory?
+          (* TODO: Can we make it so that the parenthesis above are mandatory?
              Leaving them away is inconsistent with `let ... := !"x" +ₗ #1`. *)
        delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].