diff --git a/compiler/core/CAMP/Typing/TCAMP.v b/compiler/core/CAMP/Typing/TCAMP.v
index 20e0c87e2..34c443625 100644
--- a/compiler/core/CAMP/Typing/TCAMP.v
+++ b/compiler/core/CAMP/Typing/TCAMP.v
@@ -225,17 +225,6 @@ Section TCAMP.
           inversion H0; subst; rtype_equalizer.
           subst. constructor. constructor; eauto.
         * discriminate.
-    (* pgroupBy *)
-    (* 
-    - inversion tdat; subst.
-      rtype_equalizer. subst.
-      induction dl; simpl.
-      + left; econstructor; split; eauto. econstructor; eauto.
-      + inversion H2; subst.
-        specialize (IHdl (dtcoll _ _ H4) H4).
-        destruct (IHp _ _ _ _ _ tenv H1 H3) as [[dout[camp_evaleq tx]]|[s camp_evaleq]].
-        addddmit.
-        addddmit. *)
     (* passert *)
     - destruct (IHp _ _ _ _ _ tenv H1 tdat) as [[dout[camp_evaleq tx]]|camp_evaleq];
         rewrite camp_evaleq; simpl; [|eauto].
diff --git a/compiler/core/Driver/CompCorrectness.v b/compiler/core/Driver/CompCorrectness.v
index cee891aec..9e4979425 100644
--- a/compiler/core/Driver/CompCorrectness.v
+++ b/compiler/core/Driver/CompCorrectness.v
@@ -1295,7 +1295,6 @@ Section CompCorrectness.
       unfold lift_input.
       trivial_same_query.
       assumption.
-      a dmit.
     Qed.
     *)
 
diff --git a/compiler/core/NNRCMR/Optim/NNRCMRRewrite.v b/compiler/core/NNRCMR/Optim/NNRCMRRewrite.v
index 2e13f6463..226928eb2 100644
--- a/compiler/core/NNRCMR/Optim/NNRCMRRewrite.v
+++ b/compiler/core/NNRCMR/Optim/NNRCMRRewrite.v
@@ -888,43 +888,6 @@ Section NNRCMRRewrite.
         try contradiction; try congruence.
   Qed.
 
-
-(* XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX TODO XXXXXXXXXXXXXXXXXXXXXX *)
-
-  (* (* KindOfId+M=M *) *)
-
-  (* Definition merge_mr_kindofid mr1 mr2 := *)
-  (*   if equiv_decb mr1.(mr_output) mr2.(mr_input) && is_kindofid_mr mr1 then *)
-  (*     let mr := *)
-  (*         mkMR *)
-  (*             mr1.(mr_input) *)
-  (*             mr2.(mr_output) *)
-  (*             mr2.(mr_flat_map) *)
-  (*             mr2.(mr_reduce) *)
-  (*     in *)
-  (*     Some mr *)
-  (*   else *)
-  (*     None. *)
-
-  (* Lemma merge_mr_kindofid_correct : *)
-  (*   merge_correct_singleton merge_mr_kindofid. *)
-  (* Proof. *)
-  (*   unfold merge_correct_singleton. intros m1 m2 m3. *)
-  (*   intros Hdist1 Hdist2. intros. *)
-  (*   unfold merge_mr_kindofid in H0. *)
-  (*   unfold equiv_decb in *. *)
-  (*   dest_eqdec; simpl in *. *)
-  (*   - case_eq (is_kindofid_mr m1); intros; *)
-  (*     rewrite H1 in H0; try congruence. *)
-  (*     unfold mr_chain_eval. *)
-  (*     simpl. *)
-  (*     dest_eqdec; [ | congruence ]. *)
-  (*     a.dmit. *)
-  (*   - discriminate.  *)
-  (* Qed. *)
-
-  (* map-id + id-red = map-red *)
-
   (* Java equivalent: MROptimizer.merge_id_reduce_id_dist_map *)  
   Definition merge_id_reduce_id_dist_map mr1 mr2 :=
     if equiv_decb mr1.(mr_output) mr2.(mr_input)
@@ -1483,4 +1446,3 @@ Section NNRCMRRewrite.
     get_mr_chain_vars mrl.(mr_chain).
 
 End NNRCMRRewrite.
-
diff --git a/compiler/core/Updates/UDelta.v b/compiler/core/Updates/UDelta.v
index 7ee28466d..f5780675b 100644
--- a/compiler/core/Updates/UDelta.v
+++ b/compiler/core/Updates/UDelta.v
@@ -217,8 +217,7 @@ Section UDelta.
       elim (rmap (update Δ₀) l); intros; congruence.
       rewrite H.
       destruct (rmap (update Δ₀) l); reflexivity.
-    - addddmit.  (* still need work on record update – no easy corresponding query *)
-    - simpl. addddmit.  (* still need work on compose – possibly showing an intermediate lemma that does substitute with AID. *)
+      (* TODO *)
   Qed.
    *)