@@ -66,7 +66,7 @@ elabData info syn fc (PDatadecl n t_in dcons)
66 updateContext (addTyDecl n cty) -- temporary, to check cons
66 updateContext (addTyDecl n cty) -- temporary, to check cons
67 cons <- mapM (elabCon info syn) dcons
67 cons <- mapM (elabCon info syn) dcons
68 ttag <- getName
68 ttag <- getName
69− setContext (addDatatype (Data n ttag cty cons) ctxt)
69+ updateContext (addDatatype (Data n ttag cty cons))
71elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)
71elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)
72elabCon info syn (n, t_in, fc)
72elabCon info syn (n, t_in, fc)
@@ -81,6 +81,7 @@ elabCon info syn (n, t_in, fc)
81 logLvl 2 $ "Rechecking " ++ show t'
81 logLvl 2 $ "Rechecking " ++ show t'
82 def' <- checkDef defer
82 def' <- checkDef defer
83 addDeferred def'
83 addDeferred def'
84 (cty, _) <- tclift $ recheck ctxt [] t'
85 (cty, _) <- tclift $ recheck ctxt [] t'
85 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty
86 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty
86 return (n, cty)
87 return (n, cty)