@@ -212,6 +212,7 @@ elabData info syn doc argDocs fc opts (PLaterdecl n t_in)
212212 def' <- checkDef fc defer
213213 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
214214 addDeferredTyCon def''
215+ addIBC (IBCDef n)
215216 mapM_ (elabCaseBlock info []) is
216217 (cty, _) <- recheckC fc [] t'
217218 logLvl 2 $ "---> " ++ show cty