1 files changed, 1 insertions, 10 deletions
diff --git a/src/PushButtonSynthesis/MontgomeryReduction.v b/src/PushButtonSynthesis/MontgomeryReduction.v
index d4399a743..a682aa227 100644
--- a/src/PushButtonSynthesis/MontgomeryReduction.v
+++ b/src/PushButtonSynthesis/MontgomeryReduction.v
@@ -168,13 +168,6 @@ Section rmontred.
           prefix "montred" montred
           (fun _ _ _ => @nil string).
 
-  (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like
-<<
-Lemma montred_correct res
-          (Hres : montred = Success res)
-      : montred_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res).
-    Proof using curve_good. prove_correctness (). Qed.
->> *)
   Local Ltac solve_montred_preconditions :=
     repeat first [ lia
            | apply use_curve_good
@@ -197,6 +190,4 @@ Lemma montred_correct res
     { cbv [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by bound is_bounded_by_bool value_range upper lower].
       rewrite Bool.andb_true_iff, !Z.leb_le. lia. }
   Qed.
-End rmontred.
-
-(* TODO: get Barrett to this same point, and then use these lemmas in the specific files *)
-\ No newline at end of file
+End rmontred.
+\ No newline at end of file