@@ -66,7 +66,7 @@ elabData info syn fc (PDatadecl n t_in dcons)
6666 updateContext (addTyDecl n cty) -- temporary, to check cons
6767 cons <- mapM (elabCon info syn) dcons
6868 ttag <- getName
69− setContext (addDatatype (Data n ttag cty cons) ctxt)
69+ updateContext (addDatatype (Data n ttag cty cons))
7070
7171elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)
7272elabCon info syn (n, t_in, fc)
@@ -81,6 +81,7 @@ elabCon info syn (n, t_in, fc)
8181 logLvl 2 $ "Rechecking " ++ show t'
8282 def' <- checkDef defer
8383 addDeferred def'
84+ ctxt <- getContext
8485 (cty, _) <- tclift $ recheck ctxt [] t'
8586 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty
8687 return (n, cty)