diff --git a/theories/examples/delim_lang/interp.v b/theories/examples/delim_lang/interp.v
index c049041..958bb5a 100644
--- a/theories/examples/delim_lang/interp.v
+++ b/theories/examples/delim_lang/interp.v
@@ -159,7 +159,6 @@ Section interp.
     λne env, Ret n.
 
   (** ** CONT *)
-  (** XXX DF: why do we need a tick here? Seems to be necessary for soundness *)
   Program Definition interp_cont_val {S} (K : S -n> (IT -n> IT)) : S -n> IT :=
     λne env, (λit x, Tick $ 𝒫 (K env x)).
   Solve All Obligations with solve_proper_please.
diff --git a/theories/examples/input_lang_callcc/interp.v b/theories/examples/input_lang_callcc/interp.v
index 64c8d68..757882a 100644
--- a/theories/examples/input_lang_callcc/interp.v
+++ b/theories/examples/input_lang_callcc/interp.v
@@ -3,7 +3,6 @@ From gitrees.effects Require Export callcc.
 From gitrees.examples.input_lang_callcc Require Import lang.
 Require Import Binding.Lib Binding.Set.
 
-(* XXX TODO: this duplicates wp_input and wp_output *)
 Section weakestpre.
   Context {sz : nat}.
   Variable (rs : gReifiers CtxDep sz).
diff --git a/theories/lib/factorial.v b/theories/lib/factorial.v
index 96721d3..ad4d460 100644
--- a/theories/lib/factorial.v
+++ b/theories/lib/factorial.v
@@ -67,7 +67,6 @@ Section fact.
       iNext. iNext. iIntros "Hacc".
       iApply wp_val. iModIntro.
       simpl. unfold NatOpRSCtx.
-      (* TODO: look at this with amin *)
       iAssert (IT_of_V (E:=F) (RetV m) ≡ (Ret m))%I as "#Hm".
       { iPureIntro. apply (IT_of_V_Ret (B:=R)). }
       iRewrite "Hm".