From 0a288aec400a0caef2b218b702ac932a7426bb0c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 4 Oct 2014 09:19:28 -0700
Subject: [PATCH] chore(frontends/lean/proof_qed_elaborator): remove obsolete
 comment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/proof_qed_elaborator.cpp | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/frontends/lean/proof_qed_elaborator.cpp b/src/frontends/lean/proof_qed_elaborator.cpp
index 3df7ccb32..08d91bfd8 100644
--- a/src/frontends/lean/proof_qed_elaborator.cpp
+++ b/src/frontends/lean/proof_qed_elaborator.cpp
@@ -49,8 +49,6 @@ constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr cons
                                      });
         if (im)
             im->instantiate(new_s);
-        // TODO(Leo): the solution new_s also assigns auxiliary metavariables
-        // that are needed to generate data for the info_manager
         constraints r = cls.mk_constraints(new_s, j, relax);
         return append(r, postponed);
     };