From 623ff2454b7076811084eb499bfebbb9e2f7abcc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 8 Dec 2017 11:47:20 -0800
Subject: [PATCH] chore(library/init/meta/interactive): remove TODO

We now have `whnf_ginductive`
---
 library/init/meta/interactive.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index e0c316e1a9..ab798efe33 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -453,7 +453,7 @@ do
    (e, newvars, locals) ← do {
       none ← pure rec_name | pure (e, [], []),
       t ← infer_type e,
-      -- TODO(Kha): `t ← whnf_ginductive t,`
+      t ← whnf_ginductive t,
       const n _ ← pure t.get_app_fn | pure (e, [], []),
       env ← get_env,
       tt ← pure $ env.is_inductive n | pure (e, [], []),