rm comments

logsem · Jul 9, 2024 · e54d14e · e54d14e
1 parent 1738ebc
commit e54d14e
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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".